1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
  5  -/
  6  
  7  import linear_algebra.basic linear_algebra.finsupp order.zorn
src         └──────────────────┘ └────────────────────┘ └────────┘
  8  
  9  /-!
 10  
 11  # Linear independence and bases
 12  
 13  This file defines linear independence and bases in a module or vector space.
 14  
 15  It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.
 16  
 17  ## Main definitions
 18  
 19  All definitions are given for families of vectors, i.e. `v : ι → M` where M is the module or
 20  vectorspace and `ι : Type*` is an arbitrary indexing type.
 21  
 22  * `linear_independent R v` states that the elements of the family `v` are linear independent
 23  
 24  * `linear_independent.repr hv x` returns the linear combination representing `x : span R (range v)`
 25    on the linear independent vectors `v`, given `hv : linear_independent R v`
 26    (using classical choice). `linear_independent.repr hv` is provided as a linear map.
 27  
 28  * `is_basis R v` states that the vector family `v` is a basis, i.e. it is linear independent and
 29    spans the entire space
 30  
 31  * `is_basis.repr hv x` is the basis version of `linear_independent.repr hv x`. It returns the
 32    linear combination representing `x : M` on a basis `v` of `M` (using classical choice).
 33    The argument `hv` must be a proof that `is_basis R v`. `is_basis.repr hv` is given as a linear
 34    map as well.
 35  
 36  * `is_basis.constr hv f` constructs a linear map `M₁ →ₗ[R] M₂` given the values `f : ι → M₂` at the
 37    basis `v : ι → M₁`, given `hv : is_basis R v`.
 38  
 39  ## Main statements
 40  
 41  * `is_basis.ext` states that two linear maps are equal if they coincide on a basis.
 42  
 43  * `exists_is_basis` states that every vector space has a basis.
 44  
 45  ## Implementation notes
 46  
 47  We use families instead of sets because it allows us to say that two identical vectors are linearly
 48  dependent. For bases, this is useful as well because we can easily derive ordered bases by using an
 49  ordered index type ι.
 50  
 51  If you want to use sets, use the family `(λ x, x : s → M)` given a set `s : set M`. The lemmas
 52  `linear_independent.to_subtype_range` and `linear_independent.of_subtype_range` connect those two
 53  worlds.
 54  
 55  ## Tags
 56  
 57  linearly dependent, linear dependence, linearly independent, linear independence, basis
 58  
 59  -/
 60  
 61  noncomputable theory
 62  
 63  open function lattice set submodule
 64  open_locale classical
 65  
 66  variables {ι : Type*} {ι' : Type*} {R : Type*} {K : Type*}
 67            {M : Type*} {M' : Type*} {V : Type*} {V' : Type*}
 68  
 69  section module
 70  variables {v : ι → M}
 71  variables [ring R] [add_comm_group M] [add_comm_group M']
id              └──┘    └────────────┘     └────────────┘
src             └──┘     └────────────┘     └────────────┘
typ             └──┘    └────────────┘     └────────────┘
 72  variables [module R M] [module R M']
id              └────┘       └────┘
src             └────┘       └────┘
typ             └────┘       └────┘
doc             └────┘       └────┘
 73  variables {a b : R} {x y : M}
 74  include R
 75  
 76  variables (R) (v)
 77  /-- Linearly independent family of vectors -/
 78  def linear_independent : Prop := (finsupp.total ι M R v).ker = ⊥
id                                     └───────────┘     └─┘   
src                                    └───────────┘         └─┘   
typ                                    └───────────┘     └─┘   
doc                                    └───────────┘         └─┘
 79  variables {R} {v}
 80  
 81  theorem linear_independent_iff : linear_independent R v ↔
id                                    └────────────────┘   
src                                   └────────────────┘     
typ                                   └────────────────┘   
doc                                   └────────────────┘
 82    ∀l, finsupp.total ι M R v l = 0 → l = 0 :=
id        └───────────┘            
src        └───────────┘                  
typ       └───────────┘            
doc        └───────────┘
 83  by simp [linear_independent, linear_map.ker_eq_bot']
id            └────────────────┘  └────────────────────┘
src     └────┘└────────────────┘└┘└────────────────────┘└─
typ     └────┘└────────────────┘└┘└────────────────────┘└─
doc     └────┘└────────────────┘└┘                      └─
txt     └────┘                  └┘                      └─
par     └────┘                  └┘                      └─
pid                           └┘                      
st     └──────────────────────────────────────────────────
 84  
src  
typ  
doc  
txt  
par  
pid  
st   
 85  theorem linear_independent_iff' : linear_independent R v ↔
id                                     └────────────────┘   
src                                    └────────────────┘     
typ                                    └────────────────┘   
doc                                    └────────────────┘
 86    ∀ s : finset ι, ∀ g : ι → R, s.sum (λ i, g i • v i) = 0 → ∀ i ∈ s, g i = 0 :=
id           └────┘             └──┘                          
src          └────┘                  └──┘                                  
typ          └────┘             └──┘                          
doc          └────┘
 87  linear_independent_iff.trans
id   └────────────────────┘└────┘
src  └────────────────────┘└────┘
typ  └────────────────────┘└────┘
 88  ⟨λ hf s g hg i his, have h : _ := hf (s.sum $ λ i, finsupp.single i (g i)) $
id      └┘   └┘  └─┘                └┘  └──┘       └────────────┘    
src                                         └──┘        └────────────┘
typ     └┘   └┘  └─┘                └┘  └──┘       └────────────┘    
doc                                                     └────────────┘
 89        by simpa only [linear_map.map_sum, finsupp.total_single] using hg, calc
id                        └────────────────┘  └──────────────────┘        └┘
src           └──────────┘└────────────────┘└┘└──────────────────┘└──────┘
typ           └──────────┘└────────────────┘└┘└──────────────────┘└──────┘└┘
doc           └──────────┘                  └┘                    └──────┘
txt           └──────────┘                  └┘                    └──────┘
par           └──────────┘                  └┘                    └──────┘
pid                └──┘└┘                  └┘                    └────┘
st           └─────────────────────────────────────────────────────────────┘
 90      g i = (finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (finsupp.single i (g i)) :
id            └────────────┘      └┘   └─┘    └────────────┘    
src             └────────────┘        └┘    └─┘      └────────────┘
typ           └────────────┘      └┘   └─┘    └────────────┘    
doc                                   └┘              └────────────┘
 91        by rw [finsupp.lapply_apply, finsupp.single_eq_same]
id                └──────────────────┘  └────────────────────┘
src           └──┘└──────────────────┘└┘└────────────────────┘└─
typ           └──┘└──────────────────┘└┘└────────────────────┘└─
doc           └──┘                    └┘                      └─
txt           └──┘                    └┘                      └─
par           └──┘                    └┘                      └─
pid             └┘                    └┘                      
st           └───────────────────────┘└──────────────────────┘
 92      ... = s.sum (λ j, (finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (finsupp.single j (g j))) :
id             └──┘       └────────────┘      └┘   └─┘    └────────────┘    
src  ───┘       └──┘        └────────────┘        └┘    └─┘      └────────────┘
typ  ───┘      └──┘       └────────────┘      └┘   └─┘    └────────────┘    
doc  ───┘                                         └┘              └────────────┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
 93        eq.symm $ finset.sum_eq_single i
id         └─────┘   └──────────────────┘ 
src        └─────┘   └──────────────────┘
typ        └─────┘   └──────────────────┘ 
 94          (λ j hjs hji, by rw [finsupp.lapply_apply, finsupp.single_eq_of_ne hji])
id               └─┘ └─┘         └──────────────────┘  └─────────────────────┘ └─┘
src                           └──┘└──────────────────┘└┘└─────────────────────┘   
typ              └─┘ └─┘     └──┘└──────────────────┘└┘└─────────────────────┘└─┘
doc                           └──┘                    └┘                          
txt                           └──┘                    └┘                          
par                           └──┘                    └┘                          
pid                             └┘                    └┘                          
st                           └───────────────────────┘└───────────────────────────┘
 95          (λ hnis, hnis.elim his)
id              └──┘  └──┘└───┘ └─┘
src                       └───┘
typ             └──┘  └──┘└───┘ └─┘
 96      ... = s.sum (λ j, finsupp.single j (g j)) i : (finsupp.lapply i : (ι →₀ R) →ₗ[R] R).map_sum.symm
id             └──┘      └────────────┘           └────────────┘      └┘   └─┘  └─────┘ └──┘
src             └──┘       └────────────┘               └────────────┘        └┘    └─┘    └─────┘ └──┘
typ            └──┘      └────────────┘           └────────────┘      └┘   └─┘  └─────┘ └──┘
doc                        └────────────┘                                     └┘
 97      ... = 0 : finsupp.ext_iff.1 h i,
id                 └─────────────┘   
src                └─────────────┘
typ                └─────────────┘   
 98  λ hf l hl, finsupp.ext $ λ i, classical.by_contradiction $ λ hni, hni $ hf _ _ hl _ $
id     └┘  └┘  └─────────┘       └────────────────────────┘     └─┘  └─┘   └┘     └┘
src             └─────────┘        └────────────────────────┘
typ    └┘  └┘  └─────────┘       └────────────────────────┘     └─┘  └─┘   └┘     └┘
 99    finsupp.mem_support_iff.2 hni⟩
id     └─────────────────────┘  └─┘
src    └─────────────────────┘
typ    └─────────────────────┘  └─┘
100  
101  lemma linear_independent_empty_type (h : ¬ nonempty ι) : linear_independent R v :=
id                                             └──────┘     └────────────────┘  
src                                            └──────┘      └────────────────┘
typ                                            └──────┘     └────────────────┘  
doc                                                           └────────────────┘
102  begin
st   └─────
103   rw [linear_independent_iff],
id        └────────────────────┘
src   └──┘└────────────────────┘
typ   └──┘└────────────────────┘
doc   └──┘                      
txt   └──┘                      
par   └──┘                      
pid     └┘                      
st   ──────────────────────────┘└──
104   intros,
src   └────┘
typ   └────┘
doc   └────┘
txt   └────┘
par   └────┘
st   ──────┘└─
105   ext i,
src   └───┘
typ   └───┘
doc   └───┘
txt   └───┘
par   └───┘
pid      └┘
st   ─────┘└─
106   exact false.elim (not_nonempty_iff_imp_false.1 h i)
id          └────────┘  └────────────────────────┘    
src   └────┘└────────┘ └────────────────────────┘└─┘  └┘
typ   └────┘└────────┘ └────────────────────────┘└─┘└┘
doc   └────┘                                     └─┘  └┘
txt   └────┘                                     └─┘  └┘
par   └────┘                                     └─┘  └┘
pid                                             └─┘  
st   ────────────────────────────────────────────────────┘
107  end
st   └─┘
108  
109  lemma ne_zero_of_linear_independent
110    {i : ι} (ne : 0 ≠ (1:R)) (hv : linear_independent R v) : v i ≠ 0 :=
id                                 └────────────────┘        
src                                  └────────────────┘            
typ                                └────────────────┘        
doc                                   └────────────────┘
111  λ h, ne $ eq.symm begin
id       └┘   └─────┘
src       └┘   └─────┘
typ      └┘   └─────┘
st                     └─────
112    suffices : (finsupp.single i 1 : ι →₀ R) i = 0, {simpa},
id                 └────────────┘        └┘    
src    └─────────┘ └────────────┘ └───┘ └┘ └┘ └┘   └───┘
typ    └─────────┘ └────────────┘ └───┘└┘└┘└┘   └───┘
doc    └─────────┘ └────────────┘ └───┘ └┘ └┘  └┘   └───┘
txt    └─────────┘                └───┘    └┘  └┘   └───┘
par    └─────────┘                └───┘    └┘  └┘   └───┘
pid    └───────┘└┘                └───┘    └┘  
st   ───────────────────────────────────────────────┘└──────┘└┘
113    rw linear_independent_iff.1 hv (finsupp.single i 1),
id        └────────────────────┘   └┘  └────────────┘ 
src    └─┘└────────────────────┘└─┘   └────────────┘ └─┘
typ    └─┘└────────────────────┘└─┘└┘ └────────────┘└─┘
doc    └─┘                      └─┘   └────────────┘ └─┘
txt    └─┘                      └─┘                  └─┘
par    └─┘                      └─┘                  └─┘
pid                            └─┘                  └─┘
st   ────────────────────────────────────────────────────┘└─
114    {simp},
src     └──┘
typ     └──┘
doc     └──┘
txt     └──┘
par     └──┘
st   ──────┘└┘
115    {simp [h]}
id            
src     └────┘ 
typ     └────┘
doc     └────┘ 
txt     └────┘ 
par     └────┘ 
pid          
st   ──────────┘└─
116  end
st   ──┘
117  
118  lemma linear_independent.comp
119    (h : linear_independent R v) (f : ι' → ι) (hf : injective f) : linear_independent R (v ∘ f) :=
id          └────────────────┘         └┘           └───────┘     └────────────────┘     
src         └────────────────┘                         └───────┘      └────────────────┘      
typ         └────────────────┘         └┘           └───────┘     └────────────────┘     
doc         └────────────────┘                                        └────────────────┘
120  begin
st   └─────
121    rw [linear_independent_iff, finsupp.total_comp],
id         └────────────────────┘  └────────────────┘
src    └──┘└────────────────────┘└┘└────────────────┘
typ    └──┘└────────────────────┘└┘└────────────────┘
doc    └──┘                      └┘                  
txt    └──┘                      └┘                  
par    └──┘                      └┘                  
pid      └┘                      └┘                  
st   ───────────────────────────┘└──────────────────┘└──
122    intros l hl,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
123    have h_map_domain : ∀ x, (finsupp.map_domain f l) (f x) = 0,
id                               └────────────────┘          
src    └──────────────────┘ └┘  └────────────────┘  └┘   └┘└┘
typ    └──────────────────┘ └┘  └────────────────┘ └┘  └┘└┘
doc    └──────────────────┘ └┘  └────────────────┘  └┘   └┘ └┘
txt    └──────────────────┘ └┘                      └┘   └┘ └┘
par    └──────────────────┘ └┘                      └┘   └┘ └┘
pid    └───────────────┘└─┘ └┘                      └┘   └┘ 
st   ────────────────────────────────────────────────────────────┘
124      by rw linear_independent_iff.1 h (finsupp.map_domain f l) hl; simp,
id             └────────────────────┘     └────────────────┘    └┘
src         └─┘└────────────────────┘└─┘  └────────────────┘  └┘    └──┘
typ         └─┘└────────────────────┘└─┘ └────────────────┘└┘└┘  └──┘
doc         └─┘                      └─┘  └────────────────┘  └┘    └──┘
txt         └─┘                      └─┘                      └┘    └──┘
par         └─┘                      └─┘                      └┘    └──┘
pid                                 └─┘                      └┘
st             └────────────────────┘                                      └─
125    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
126    convert h_map_domain a,
id             └──────────┘ 
src    └──────┘            
typ    └──────┘└──────────┘
doc    └──────┘            
txt    └──────┘            
par    └──────┘            
pid                       
st   ───────────────────────┘└─
127    simp only [finsupp.map_domain_apply hf],
id                └──────────────────────┘ └┘
src    └─────────┘└──────────────────────┘  
typ    └─────────┘└──────────────────────┘└┘
doc    └─────────┘                          
txt    └─────────┘                          
par    └─────────┘                          
pid        └──┘└┘                          
st   ────────────────────────────────────────┘└─
128  end
st   ──┘
129  
130  lemma linear_independent_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : linear_independent R v :=
id                                                                       └────────────────┘  
src                                                                       └────────────────┘
typ                                                                      └────────────────┘  
doc                                                                        └────────────────┘
131  linear_independent_iff.2 (λ l hl, finsupp.eq_zero_of_zero_eq_one zero_eq_one _)
id   └────────────────────┘      └┘  └────────────────────────────┘ └─────────┘
src  └────────────────────┘           └────────────────────────────┘
typ  └────────────────────┘      └┘  └────────────────────────────┘ └─────────┘
132  
133  lemma linear_independent.unique (hv : linear_independent R v) {l₁ l₂ : ι →₀ R} :
id                                         └────────────────┘              └┘ 
src                                        └────────────────┘                 └┘
typ                                        └────────────────┘              └┘ 
doc                                        └────────────────┘                 └┘
134    finsupp.total ι M R v l₁ = finsupp.total ι M R v l₂ → l₁ = l₂ :=
id     └───────────┘     └┘  └───────────┘     └┘   └┘  └┘
src    └───────────┘             └───────────┘                 
typ    └───────────┘     └┘  └───────────┘     └┘   └┘  └┘
doc    └───────────┘              └───────────┘
135  by apply linear_map.ker_eq_bot.1 hv
id            └───────────────────┘   └┘
src     └────┘└───────────────────┘└─┘  
typ     └────┘└───────────────────┘└─┘└┘
doc     └────┘                     └─┘  
txt     └────┘                     └─┘  
par     └────┘                     └─┘  
pid                               └─┘  
st     └─────────────────────────────────
136  
src  
typ  
doc  
txt  
par  
pid  
st   
137  lemma linear_independent.injective (zero_ne_one : (0 : R) ≠ 1) (hv : linear_independent R v) :
id                                                                      └────────────────┘  
src                                                                      └────────────────┘
typ                                                                     └────────────────┘  
doc                                                                       └────────────────┘
138    injective v :=
id     └───────┘ 
src    └───────┘
typ    └───────┘ 
139  begin
st   └─────
140    intros i j hij,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid          └──────┘
st   ───────────────┘└─
141    let l : ι →₀ R := finsupp.single i (1 : R) - finsupp.single j 1,
id              └┘                             └────────────┘ 
src    └──────┘ └┘ └──┘                └──┘ └┘└────────────┘ └┘
typ    └──────┘└┘└──┘               └──┘└┘└────────────┘└┘
doc    └──────┘ └┘ └──┘                └──┘ └┘ └────────────┘ └┘
txt    └──────┘    └──┘                └──┘ └┘                └┘
par    └──────┘    └──┘                └──┘ └┘                └┘
pid    └───┘└─┘    └──┘                └──┘ └┘                
st   ────────────────────────────────────────────────────────────────┘└─
142    have h_total : finsupp.total ι M R v l = 0,
id                    └───────────┘      
src    └─────────────┘└───────────┘     └┘
typ    └─────────────┘└───────────┘└┘
doc    └─────────────┘└───────────┘      └┘
txt    └─────────────┘                   └┘
par    └─────────────┘                   └┘
pid    └──────────┘└─┘                   
st   ───────────────────────────────────────────┘└─
143    { rw finsupp.total_apply,
id          └─────────────────┘
src      └─┘└─────────────────┘
typ      └─┘└─────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└────────────────────┘└─
144      rw finsupp.sum_sub_index,
id          └───────────────────┘
src      └─┘└───────────────────┘
typ      └─┘└───────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────────┘└─
145      { simp [finsupp.sum_single_index, hij] },
id               └──────────────────────┘  └─┘
src        └────┘└──────────────────────┘└┘   └┘
typ        └────┘└──────────────────────┘└┘└─┘└┘
doc        └────┘                        └┘   └┘
txt        └────┘                        └┘   └┘
par        └────┘                        └┘   └┘
pid                                    └┘   
st   ─────┘└───────────────────────────────────┘└┘
146      { intros, apply sub_smul } },
id                       └──────┘
src        └────┘  └────┘└──────┘
typ        └────┘  └────┘└──────┘
doc        └────┘  └────┘        
txt        └────┘  └────┘        
par        └────┘  └────┘        
pid                             
st   ───────────┘└───────────────┘└──┘
147    have h_single_eq : finsupp.single i (1 : R) = finsupp.single j 1,
id                                                 └────────────┘ 
src    └─────────────────┘                └──┘ └┘ └────────────┘ └┘
typ    └─────────────────┘               └──┘└┘ └────────────┘└┘
doc    └─────────────────┘                └──┘ └┘ └────────────┘ └┘
txt    └─────────────────┘                └──┘ └┘                └┘
par    └─────────────────┘                └──┘ └┘                └┘
pid    └──────────────┘└─┘                └──┘ └┘                
st   ─────────────────────────────────────────────────────────────────┘└─
148    { rw linear_independent_iff at hv,
id          └────────────────────┘
src      └─┘└────────────────────┘└────┘
typ      └─┘└────────────────────┘└────┘
doc      └─┘                      └────┘
txt      └─┘                      └────┘
par      └─┘                      └────┘
pid                              └────┘
st   ───┘└─────────────────────────────┘└─
149      simp [eq_add_of_sub_eq' (hv l h_total)] },
id             └───────────────┘  └┘  └─────┘
src      └────┘└───────────────┘           └─┘
typ      └────┘└───────────────┘ └┘└─────┘└─┘
doc      └────┘                            └─┘
txt      └────┘                            └─┘
par      └────┘                            └─┘
pid                                      └┘
st   ───────────────────────────────────────────┘└┘
150    show i = j,
id             
src    └───┘  
typ    └───┘ 
doc    └───┘  
txt    └───┘  
par    └───┘  
pid    └───┘  
st   ──────────────
151    { apply or.elim ((finsupp.single_eq_single_iff _ _ _ _).1 h_single_eq),
id             └─────┘   └──────────────────────────┘            └─────────┘
src      └────┘└─────┘  └──────────────────────────┘└──────────┘           
typ      └────┘└─────┘  └──────────────────────────┘└──────────┘└─────────┘
doc      └────┘                                     └──────────┘           
txt      └────┘                                     └──────────┘           
par      └────┘                                     └──────────┘           
pid                                                └──────────┘           
st   ───────────────────────────────────────────────────────────────────────┘└─
152      simp,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
153      exact λ h, false.elim (zero_ne_one.symm h.1) }
id                  └────────┘  └──────────────┘
src      └────┘ └──┘└────────┘ └──────────────┘ └──┘
typ      └────┘ └──┘└────────┘ └──────────────┘ └──┘
doc      └────┘ └──┘                            └──┘
txt      └────┘ └──┘                            └──┘
par      └────┘ └──┘                            └──┘
pid            └──┘                            └─┘
st   ────────────────────────────────────────────────┘└─
154  end
st   ──┘
155  
156  lemma linear_independent_span (hs : linear_independent R v) :
id                                       └────────────────┘  
src                                      └────────────────┘
typ                                      └────────────────┘  
doc                                      └────────────────┘
157    @linear_independent ι R (span R (range v))
id      └────────────────┘    └──┘   └───┘ 
src     └────────────────┘      └──┘    └───┘
typ     └────────────────┘    └──┘   └───┘ 
doc     └────────────────┘      └──┘    └───┘
158        (λ i : ι, ⟨v i, subset_span (mem_range_self i)⟩) _ _ _ :=
id                      └─────────┘  └────────────┘ 
src                        └─────────┘  └────────────┘
typ                     └─────────┘  └────────────┘ 
159  begin
st   └─────
160    rw linear_independent_iff at *,
id        └────────────────────┘
src    └─┘└────────────────────┘└───┘
typ    └─┘└────────────────────┘└───┘
doc    └─┘                      └───┘
txt    └─┘                      └───┘
par    └─┘                      └───┘
pid                            └───┘
st   ───────────────────────────────┘└─
161    intros l hl,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
162    apply hs l,
id           └┘ 
src    └────┘  
typ    └────┘└┘
doc    └────┘  
txt    └────┘  
par    └────┘  
pid           
st   ───────────┘└─
163    have := congr_arg (submodule.subtype (span R (range v))) hl,
id             └───────┘  └───────────────┘  └──┘   └───┘     └┘
src    └──────┘└───────┘ └───────────────┘ └──┘  └───┘ └──┘
typ    └──────┘└───────┘ └───────────────┘ └──┘ └───┘└──┘└┘
doc    └──────┘                            └──┘  └───┘ └──┘
txt    └──────┘                                        └──┘
par    └──────┘                                        └──┘
pid    └───┘└─┘                                        └──┘
st   ────────────────────────────────────────────────────────────┘└─
164    convert this,
id             └──┘
src    └──────┘
typ    └──────┘└──┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ─────────────┘└─
165    rw [finsupp.total_apply, finsupp.total_apply],
id         └─────────────────┘  └─────────────────┘
src    └──┘└─────────────────┘└┘└─────────────────┘
typ    └──┘└─────────────────┘└┘└─────────────────┘
doc    └──┘                   └┘                   
txt    └──┘                   └┘                   
par    └──┘                   └┘                   
pid      └┘                   └┘                   
st   ────────────────────────┘└───────────────────┘└──
166    unfold finsupp.sum,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid          └──────────┘
st   ───────────────────┘└─
167    rw linear_map.map_sum (submodule.subtype (span R (range v))),
id        └────────────────┘  └───────────────┘  └──┘   └───┘ 
src    └─┘└────────────────┘ └───────────────┘ └──┘  └───┘ └─┘
typ    └─┘└────────────────┘ └───────────────┘ └──┘ └───┘└─┘
doc    └─┘                                     └──┘  └───┘ └─┘
txt    └─┘                                                 └─┘
par    └─┘                                                 └─┘
pid                                                       └─┘
st   ─────────────────────────────────────────────────────────────┘└─
168    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
169  end
st   └─┘
170  
171  section subtype
172  /- The following lemmas use the subtype defined by a set in M as the index set ι. -/
173  
174  theorem linear_independent_comp_subtype {s : set ι} :
id                                                └─┘ 
src                                               └─┘
typ                                               └─┘ 
175    linear_independent R (v ∘ subtype.val : s → M) ↔
id     └────────────────┘     └─────────┘        
src    └────────────────┘       └─────────┘          
typ    └────────────────┘     └─────────┘        
doc    └────────────────┘
176    ∀ l ∈ (finsupp.supported R R s), (finsupp.total ι M R v) l = 0 → l = 0 :=
id           └───────────────┘       └───────────┘             
src           └───────────────┘          └───────────┘                   
typ          └───────────────┘       └───────────┘             
doc                                      └───────────┘
177  begin
st   └─────
178    rw [linear_independent_iff, finsupp.total_comp],
id         └────────────────────┘  └────────────────┘
src    └──┘└────────────────────┘└┘└────────────────┘
typ    └──┘└────────────────────┘└┘└────────────────┘
doc    └──┘                      └┘                  
txt    └──┘                      └┘                  
par    └──┘                      └┘                  
pid      └┘                      └┘                  
st   ───────────────────────────┘└──────────────────┘└──
179    simp only [linear_map.comp_apply],
id                └───────────────────┘
src    └─────────┘└───────────────────┘
typ    └─────────┘└───────────────────┘
doc    └─────────┘                     
txt    └─────────┘                     
par    └─────────┘                     
pid        └──┘└┘                     
st   ──────────────────────────────────┘└─
180    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
181    { intros h l hl₁ hl₂,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid            └──────────┘
st   ───┘└────────────────┘└─
182      have h_bij : bij_on subtype.val (subtype.val ⁻¹' l.support.to_set : set s) l.support.to_set,
id                    └────┘              └─────────┘ └─┘                    └─┘   └──────────────┘
src      └───────────┘└────┘            └─────────┘└─┘                └─┘└─┘ └┘└──────────────┘
typ      └───────────┘└────┘            └─────────┘└─┘                └─┘└─┘└┘└──────────────┘
doc      └───────────┘└────┘                       └─┘                └─┘    └┘└──────────────┘
txt      └───────────┘                                                └─┘    └┘
par      └───────────┘                                                └─┘    └┘
pid      └────────┘└─┘                                                └─┘    └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
183      { apply bij_on.mk,
id               └───────┘
src        └────┘└───────┘
typ        └────┘└───────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└─────────────┘└─
184        { unfold maps_to },
src          └─────────────┘
typ          └─────────────┘
doc          └─────────────┘
txt          └─────────────┘
par          └─────────────┘
pid                └──────┘
st   ───────┘└─────────────┘└┘
185        { apply set.inj_on_of_injective _ subtype.val_injective },
id                 └─────────────────────┘   └───────────────────┘
src          └────┘└─────────────────────┘└─┘└───────────────────┘
typ          └────┘└─────────────────────┘└─┘└───────────────────┘
doc          └────┘                       └─┘                     
txt          └────┘                       └─┘                     
par          └────┘                       └─┘                     
pid                                      └─┘                     
st   ───────┘└────────────────────────────────────────────────────┘└┘
186        intros i hi,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid              └───┘
st   ────────────────┘└─
187        rw mem_image,
id            └───────┘
src        └─┘└───────┘
typ        └─┘└───────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────────────┘└─
188        use subtype.mk i (((finsupp.mem_supported _ _).1 hl₁ : ↑(l.support) ⊆ s) hi),
id             └────────┘     └───────────────────┘        └─┘    └───────┘     └┘
src        └──┘└────────┘    └───────────────────┘└──────┘   └─┘ └───────┘└┘ └┘  
typ        └──┘└────────┘   └───────────────────┘└──────┘└─┘└─┘ └───────┘└┘└┘└┘
doc        └──┘                                   └──────┘   └─┘           └┘  └┘  
txt        └──┘                                   └──────┘   └─┘           └┘  └┘  
par        └──┘                                   └──────┘   └─┘           └┘  └┘  
pid                                              └──────┘   └─┘           └┘  └┘  
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
189        rw mem_preimage,
id            └──────────┘
src        └─┘└──────────┘
typ        └─┘└──────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────────────────────┘└─
190        exact ⟨hi, rfl⟩ },
id                └┘  └─┘
src        └────┘   └┘└─┘└┘
typ        └────┘ └┘└┘└─┘└┘
doc        └────┘   └┘   └┘
txt        └────┘   └┘   └┘
par        └────┘   └┘   └┘
pid                └┘   
st   ─────────────────────┘└┘
191      show l = 0,
id             
src      └───┘ └┘
typ      └───┘└┘
doc      └───┘  └┘
txt      └───┘  └┘
par      └───┘  └┘
pid      └───┘  
st   ────────────────
192      { apply finsupp.eq_zero_of_comap_domain_eq_zero (subtype.val : s → ι) _ h_bij,
id               └─────────────────────────────────────┘  └─────────┘          └───┘
src        └────┘└─────────────────────────────────────┘ └─────────┘└─┘   └──┘
typ        └────┘└─────────────────────────────────────┘ └─────────┘└─┘ └──┘└───┘
doc        └────┘                                                   └─┘   └──┘
txt        └────┘                                                   └─┘   └──┘
par        └────┘                                                   └─┘   └──┘
pid                                                                └─┘   └──┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
193        apply h,
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────┘└─
194        convert hl₂,
id                 └─┘
src        └──────┘
typ        └──────┘└─┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid               
st   ────────────────┘└─
195        rw [finsupp.lmap_domain_apply, finsupp.map_domain_comap_domain],
id             └───────────────────────┘  └─────────────────────────────┘
src        └──┘└───────────────────────┘└┘└─────────────────────────────┘
typ        └──┘└───────────────────────┘└┘└─────────────────────────────┘
doc        └──┘                         └┘                               
txt        └──┘                         └┘                               
par        └──┘                         └┘                               
pid          └┘                         └┘                               
st   ──────────────────────────────────┘└───────────────────────────────┘└──
196        apply subtype.val_injective,
id               └───────────────────┘
src        └────┘└───────────────────┘
typ        └────┘└───────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────────┘└─
197        rw subtype.range_val,
id            └───────────────┘
src        └─┘└───────────────┘
typ        └─┘└───────────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────────────────────────┘└─
198        exact (finsupp.mem_supported _ _).1 hl₁ } },
id                └───────────────────┘        └─┘
src        └────┘ └───────────────────┘└──────┘   
typ        └────┘ └───────────────────┘└──────┘└─┘
doc        └────┘                      └──────┘   
txt        └────┘                      └──────┘   
par        └────┘                      └──────┘   
pid                                   └──────┘   
st   ─────────────────────────────────────────────┘└──┘
199    { intros h l hl,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid            └─────┘
st   ────────────────┘└─
200      have hl' : finsupp.total ι M R v (finsupp.emb_domain ⟨subtype.val, subtype.val_injective⟩ l) = 0,
id                  └───────────┘      └────────────────┘  └─────────┘  └───────────────────┘  
src      └─────────┘└───────────┘     └────────────────┘ └─────────┘└┘└───────────────────┘└┘ └┘ └┘
typ      └─────────┘└───────────┘ └────────────────┘ └─────────┘└┘└───────────────────┘└┘└┘ └┘
doc      └─────────┘└───────────┘     └────────────────┘            └┘                     └┘ └┘ └┘
txt      └─────────┘                                                └┘                     └┘ └┘ └┘
par      └─────────┘                                                └┘                     └┘ └┘ └┘
pid      └──────┘└─┘                                                └┘                     └┘ └┘ 
st   ───────────────────────────────────────────────────────────────────────────────────────────────────┘└─
201      { rw finsupp.emb_domain_eq_map_domain ⟨subtype.val, subtype.val_injective⟩ l,
id            └──────────────────────────────┘  └─────────┘  └───────────────────┘  
src        └─┘└──────────────────────────────┘ └─────────┘└┘└───────────────────┘└┘
typ        └─┘└──────────────────────────────┘ └─────────┘└┘└───────────────────┘└┘
doc        └─┘                                            └┘                     └┘
txt        └─┘                                            └┘                     └┘
par        └─┘                                            └┘                     └┘
pid                                                      └┘                     └┘
st   ─────┘└────────────────────────────────────────────────────────────────────────┘└─
202        apply hl },
src        └────┘  
typ        └────┘  
doc        └────┘  
txt        └────┘  
par        └────┘  
pid               
st   ──────────────┘└┘
203      apply finsupp.emb_domain_inj.1,
id             └────────────────────┘
src      └────┘└────────────────────┘└┘
typ      └────┘└────────────────────┘└┘
doc      └────┘                      └┘
txt      └────┘                      └┘
par      └────┘                      └┘
pid                                 └┘
st   ─────────────────────────────────┘└─
204      rw [h (finsupp.emb_domain ⟨subtype.val, subtype.val_injective⟩ l) _ hl',
id             └────────────────┘  └─────────┘  └───────────────────┘      └─┘
src      └──┘  └────────────────┘ └─────────┘└┘└───────────────────┘└┘ └──┘   └─
typ      └──┘ └────────────────┘ └─────────┘└┘└───────────────────┘└┘└──┘└─┘└─
doc      └──┘  └────────────────┘            └┘                     └┘ └──┘   └─
txt      └──┘                                └┘                     └┘ └──┘   └─
par      └──┘                                └┘                     └┘ └──┘   └─
pid        └┘                                └┘                     └┘ └──┘   └─
st   ──────────────────────────────────────────────────────────────────────────┘└─
205          finsupp.emb_domain_zero],
id           └─────────────────────┘
src  ───────┘└─────────────────────┘
typ  ───────┘└─────────────────────┘
doc  ───────┘                       
txt  ───────┘                       
par  ───────┘                       
pid  ───────┘                       
st   ──────────────────────────────┘└──
206      rw [finsupp.mem_supported, finsupp.support_emb_domain],
id           └───────────────────┘  └────────────────────────┘
src      └──┘└───────────────────┘└┘└────────────────────────┘
typ      └──┘└───────────────────┘└┘└────────────────────────┘
doc      └──┘                     └┘                          
txt      └──┘                     └┘                          
par      └──┘                     └┘                          
pid        └┘                     └┘                          
st   ────────────────────────────┘└──────────────────────────┘└──
207      intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
208      rw [finset.mem_coe, finset.mem_map] at hx,
id           └────────────┘  └────────────┘
src      └──┘└────────────┘└┘└────────────┘└─────┘
typ      └──┘└────────────┘└┘└────────────┘└─────┘
doc      └──┘              └┘              └─────┘
txt      └──┘              └┘              └─────┘
par      └──┘              └┘              └─────┘
pid        └┘              └┘              └────┘
st   ─────────────────────┘└──────────────┘└────┘└─
209      rcases hx with ⟨i, x', hx'⟩,
id              └┘
src      └─────┘  └────────────────┘
typ      └─────┘└┘└────────────────┘
doc      └─────┘  └────────────────┘
txt      └─────┘  └────────────────┘
par      └─────┘  └────────────────┘
pid              └────────────────┘
st   ──────────────────────────────┘└─
210      rw ←hx',
id           └─┘
src      └──┘
typ      └──┘└─┘
doc      └──┘
txt      └──┘
par      └──┘
pid        └┘
st   ──────────┘└─
211      simp }
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└─
212  end
st   ──┘
213  
214  theorem linear_independent_subtype {s : set M} :
id                                           └─┘ 
src                                          └─┘
typ                                          └─┘ 
215    linear_independent R (λ x, x : s → M) ↔
id     └────────────────┘               
src    └────────────────┘                    
typ    └────────────────┘               
doc    └────────────────┘
216    ∀ l ∈ (finsupp.supported R R s), (finsupp.total M M R id) l = 0 → l = 0 :=
id           └───────────────┘       └───────────┘    └┘         
src           └───────────────┘          └───────────┘       └┘           
typ          └───────────────┘       └───────────┘    └┘         
doc                                      └───────────┘
217  by apply @linear_independent_comp_subtype _ _ _ id
id             └─────────────────────────────┘       └┘
src     └────┘ └─────────────────────────────┘└─────┘└┘
typ     └────┘ └─────────────────────────────┘└─────┘└┘
doc     └────┘                                └─────┘  
txt     └────┘                                └─────┘  
par     └────┘                                └─────┘  
pid                                          └─────┘  
st     └────────────────────────────────────────────────
218  
src  
typ  
doc  
txt  
par  
pid  
st   
219  theorem linear_independent_comp_subtype_disjoint {s : set ι} :
id                                                         └─┘ 
src                                                        └─┘
typ                                                        └─┘ 
220    linear_independent R (v ∘ subtype.val : s → M) ↔
id     └────────────────┘     └─────────┘        
src    └────────────────┘       └─────────┘          
typ    └────────────────┘     └─────────┘        
doc    └────────────────┘
221    disjoint (finsupp.supported R R s) (finsupp.total ι M R v).ker :=
id     └──────┘  └───────────────┘      └───────────┘     └─┘
src    └──────┘  └───────────────┘         └───────────┘         └─┘
typ    └──────┘  └───────────────┘      └───────────┘     └─┘
doc    └──────┘                            └───────────┘         └─┘
222  by rw [linear_independent_comp_subtype, linear_map.disjoint_ker]
id          └─────────────────────────────┘  └─────────────────────┘
src     └──┘└─────────────────────────────┘└┘└─────────────────────┘└─
typ     └──┘└─────────────────────────────┘└┘└─────────────────────┘└─
doc     └──┘                               └┘                       └─
txt     └──┘                               └┘                       └─
par     └──┘                               └┘                       └─
pid       └┘                               └┘                       
st     └──────────────────────────────────┘└───────────────────────┘
223  
src  
typ  
doc  
txt  
par  
pid  
st   
224  theorem linear_independent_subtype_disjoint {s : set M} :
id                                                    └─┘ 
src                                                   └─┘
typ                                                   └─┘ 
225    linear_independent R (λ x, x : s → M) ↔
id     └────────────────┘               
src    └────────────────┘                    
typ    └────────────────┘               
doc    └────────────────┘
226    disjoint (finsupp.supported R R s) (finsupp.total M M R id).ker :=
id     └──────┘  └───────────────┘      └───────────┘    └┘ └─┘
src    └──────┘  └───────────────┘         └───────────┘       └┘ └─┘
typ    └──────┘  └───────────────┘      └───────────┘    └┘ └─┘
doc    └──────┘                            └───────────┘          └─┘
227  by apply @linear_independent_comp_subtype_disjoint _ _ _ id
id             └──────────────────────────────────────┘       └┘
src     └────┘ └──────────────────────────────────────┘└─────┘└┘
typ     └────┘ └──────────────────────────────────────┘└─────┘└┘
doc     └────┘                                         └─────┘  
txt     └────┘                                         └─────┘  
par     └────┘                                         └─────┘  
pid                                                   └─────┘  
st     └─────────────────────────────────────────────────────────
228  
src  
typ  
doc  
txt  
par  
pid  
st   
229  theorem linear_independent_iff_total_on {s : set M} :
id                                                └─┘ 
src                                               └─┘
typ                                               └─┘ 
230    linear_independent R (λ x, x : s → M) ↔ (finsupp.total_on M M R id s).ker = ⊥ :=
id     └────────────────┘                 └──────────────┘    └┘  └─┘   
src    └────────────────┘                      └──────────────┘       └┘   └─┘   
typ    └────────────────┘                 └──────────────┘    └┘  └─┘   
doc    └────────────────┘                                                   └─┘
231  by rw [finsupp.total_on, linear_map.ker, linear_map.comap_cod_restrict, map_bot, comap_bot,
id          └──────────────┘  └────────────┘  └───────────────────────────┘  └─────┘  └───────┘
src     └──┘└──────────────┘└┘└────────────┘└┘└───────────────────────────┘└┘└─────┘└┘└───────┘└─
typ     └──┘└──────────────┘└┘└────────────┘└┘└───────────────────────────┘└┘└─────┘└┘└───────┘└─
doc     └──┘                └┘└────────────┘└┘                             └┘       └┘         └─
txt     └──┘                └┘              └┘                             └┘       └┘         └─
par     └──┘                └┘              └┘                             └┘       └┘         └─
pid       └┘                └┘              └┘                             └┘       └┘         └─
st     └───────────────────┘└──────────────┘└─────────────────────────────┘└───────┘└─────────┘└─
232    linear_map.ker_comp, linear_independent_subtype_disjoint, disjoint, ← map_comap_subtype,
id     └─────────────────┘  └─────────────────────────────────┘  └──────┘    └───────────────┘
src  ─┘└─────────────────┘└┘└─────────────────────────────────┘└┘└──────┘└──┘└───────────────┘└─
typ  ─┘└─────────────────┘└┘└─────────────────────────────────┘└┘└──────┘└──┘└───────────────┘└─
doc  ─┘                   └┘                                   └┘└──────┘└──┘                 └─
txt  ─┘                   └┘                                   └┘        └──┘                 └─
par  ─┘                   └┘                                   └┘        └──┘                 └─
pid  ─┘                   └┘                                   └┘        └──┘                 └─
st   ────────────────────┘└───────────────────────────────────┘└────────┘└───────────────────┘└─
233    map_le_iff_le_comap, comap_bot, ker_subtype, le_bot_iff]
id     └─────────────────┘  └───────┘  └─────────┘  └────────┘
src  ─┘└─────────────────┘└┘└───────┘└┘└─────────┘└┘└────────┘└─
typ  ─┘└─────────────────┘└┘└───────┘└┘└─────────┘└┘└────────┘└─
doc  ─┘                   └┘         └┘           └┘          └─
txt  ─┘                   └┘         └┘           └┘          └─
par  ─┘                   └┘         └┘           └┘          └─
pid  ─┘                   └┘         └┘           └┘          
st   ────────────────────┘└─────────┘└───────────┘└──────────┘
234  
src  
typ  
doc  
txt  
par  
pid  
st   
235  lemma linear_independent.to_subtype_range
236    (hv : linear_independent R v) : linear_independent R (λ x, x : range v → M) :=
id           └────────────────┘      └────────────────┘          └───┘    
src          └────────────────┘        └────────────────┘             └───┘
typ          └────────────────┘      └────────────────┘          └───┘    
doc          └────────────────┘        └────────────────┘             └───┘
237  begin
st   └─────
238    by_cases zero_eq_one : (0 : R) = 1,
id                                   
src    └───────┘           └─┘ └──┘ └┘└┘
typ    └───────┘           └─┘ └──┘└┘└┘
doc    └───────┘           └─┘ └──┘ └┘ └┘
txt    └───────┘           └─┘ └──┘ └┘ └┘
par    └───────┘           └─┘ └──┘ └┘ └┘
pid                       └─┘ └──┘ └┘ 
st   ───────────────────────────────────┘└─
239    { apply linear_independent_of_zero_eq_one zero_eq_one },
id             └───────────────────────────────┘ └─────────┘
src      └────┘└───────────────────────────────┘           
typ      └────┘└───────────────────────────────┘└─────────┘
doc      └────┘                                            
txt      └────┘                                            
par      └────┘                                            
pid                                                       
st   ───┘└──────────────────────────────────────────────────┘└┘
240    rw linear_independent_subtype,
id        └────────────────────────┘
src    └─┘└────────────────────────┘
typ    └─┘└────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────────────┘└─
241    intros l hl₁ hl₂,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
242    have h_bij : bij_on v (v ⁻¹' finset.to_set (l.support)) (finset.to_set (l.support)),
id                  └────┘     └─┘                             └───────────┘  └───────┘
src    └───────────┘└────┘   └─┘                       └─┘ └───────────┘ └───────┘└┘
typ    └───────────┘└────┘  └─┘                       └─┘ └───────────┘ └───────┘└┘
doc    └───────────┘└────┘   └─┘                       └─┘ └───────────┘          └┘
txt    └───────────┘                                   └─┘                        └┘
par    └───────────┘                                   └─┘                        └┘
pid    └────────┘└─┘                                   └─┘                        └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
243    { apply bij_on.mk,
id             └───────┘
src      └────┘└───────┘
typ      └────┘└───────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────────────┘└─
244      { unfold maps_to },
src        └─────────────┘
typ        └─────────────┘
doc        └─────────────┘
txt        └─────────────┘
par        └─────────────┘
pid              └──────┘
st   ─────┘└─────────────┘└┘
245      { apply set.inj_on_of_injective _ (linear_independent.injective zero_eq_one hv) },
id               └─────────────────────┘    └──────────────────────────┘ └─────────┘ └┘
src        └────┘└─────────────────────┘└─┘ └──────────────────────────┘             └┘
typ        └────┘└─────────────────────┘└─┘ └──────────────────────────┘└─────────┘└┘└┘
doc        └────┘                       └─┘                                          └┘
txt        └────┘                       └─┘                                          └┘
par        └────┘                       └─┘                                          └┘
pid                                    └─┘                                          
st   ─────┘└────────────────────────────────────────────────────────────────────────────┘└┘
246      intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
247      rcases mem_range.1 (((finsupp.mem_supported _ _).1 hl₁ : ↑(l.support) ⊆ range v) hx) with ⟨i, hi⟩,
id              └───────┘      └───────────────────┘        └─┘    └───────┘   └───┘   └┘
src      └─────┘└───────┘└─┘   └───────────────────┘└──────┘   └─┘ └───────┘└┘└───┘ └┘  └────────────┘
typ      └─────┘└───────┘└─┘   └───────────────────┘└──────┘└─┘└─┘ └───────┘└┘└───┘└┘└┘└────────────┘
doc      └─────┘         └─┘                        └──────┘   └─┘           └┘ └───┘ └┘  └────────────┘
txt      └─────┘         └─┘                        └──────┘   └─┘           └┘       └┘  └────────────┘
par      └─────┘         └─┘                        └──────┘   └─┘           └┘       └┘  └────────────┘
pid                     └─┘                        └──────┘   └─┘           └┘       └┘  └────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
248      rw mem_image,
id          └───────┘
src      └─┘└───────┘
typ      └─┘└───────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────┘└─
249      use i,
id           
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
pid         
st   ────────┘└─
250      rw [mem_preimage, hi],
id           └──────────┘  └┘
src      └──┘└──────────┘└┘  
typ      └──┘└──────────┘└┘└┘
doc      └──┘            └┘  
txt      └──┘            └┘  
par      └──┘            └┘  
pid        └┘            └┘  
st   ───────────────────┘└──┘└──
251      exact ⟨hx, rfl⟩ },
id              └┘  └─┘
src      └────┘   └┘└─┘└┘
typ      └────┘ └┘└┘└─┘└┘
doc      └────┘   └┘   └┘
txt      └────┘   └┘   └┘
par      └────┘   └┘   └┘
pid              └┘   
st   ───────────────────┘└┘
252    apply finsupp.eq_zero_of_comap_domain_eq_zero v l,
id           └─────────────────────────────────────┘  
src    └────┘└─────────────────────────────────────┘ 
typ    └────┘└─────────────────────────────────────┘
doc    └────┘                                        
txt    └────┘                                        
par    └────┘                                        
pid                                                 
st   ──────────────────────────────────────────────────┘└─
253    apply linear_independent_iff.1 hv,
id           └────────────────────┘   └┘
src    └────┘└────────────────────┘└─┘
typ    └────┘└────────────────────┘└─┘└┘
doc    └────┘                      └─┘
txt    └────┘                      └─┘
par    └────┘                      └─┘
pid                               └─┘
st   ──────────────────────────────────┘└─
254    rw [finsupp.total_comap_domain, finset.sum_preimage v l.support h_bij (λ (x : M), l x • x)],
id         └────────────────────────┘  └─────────────────┘  └───────┘ └───┘               
src    └──┘└────────────────────────┘└┘└─────────────────┘ └───────┘       └────┘ └─┘   └┘
typ    └──┘└────────────────────────┘└┘└─────────────────┘└───────┘└───┘  └────┘└─┘  └┘
doc    └──┘                          └┘                                    └────┘ └─┘    └┘
txt    └──┘                          └┘                                    └────┘ └─┘    └┘
par    └──┘                          └┘                                    └────┘ └─┘    └┘
pid      └┘                          └┘                                    └────┘ └─┘    └┘
st   ───────────────────────────────┘└──────────────────────────────────────────────────────────┘└──
255    rw [finsupp.total_apply, finsupp.sum] at hl₂,
id         └─────────────────┘  └─────────┘
src    └──┘└─────────────────┘└┘└─────────┘└──────┘
typ    └──┘└─────────────────┘└┘└─────────┘└──────┘
doc    └──┘                   └┘└─────────┘└──────┘
txt    └──┘                   └┘           └──────┘
par    └──┘                   └┘           └──────┘
pid      └┘                   └┘           └─────┘
st   ────────────────────────┘└───────────┘└─────┘└─
256    apply hl₂
src    └────┘   
typ    └────┘   
doc    └────┘   
txt    └────┘   
par    └────┘   
pid            
st   ───────────┘
257  end
st   └─┘
258  
259  lemma linear_independent.of_subtype_range (hv : injective v)
id                                                   └───────┘ 
src                                                  └───────┘
typ                                                  └───────┘ 
260    (h : linear_independent R (λ x, x : range v → M)) : linear_independent R v :=
id          └────────────────┘          └───┘         └────────────────┘  
src         └────────────────┘             └───┘           └────────────────┘
typ         └────────────────┘          └───┘         └────────────────┘  
doc         └────────────────┘             └───┘           └────────────────┘
261  begin
st   └─────
262    rw linear_independent_iff,
id        └────────────────────┘
src    └─┘└────────────────────┘
typ    └─┘└────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────────┘└─
263    intros l hl,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
264    apply finsupp.injective_map_domain hv,
id           └──────────────────────────┘ └┘
src    └────┘└──────────────────────────┘
typ    └────┘└──────────────────────────┘└┘
doc    └────┘                            
txt    └────┘                            
par    └────┘                            
pid                                     
st   ──────────────────────────────────────┘└─
265    apply linear_independent_subtype.1 h (l.map_domain v),
id           └────────────────────────┘     └──────────┘ 
src    └────┘└────────────────────────┘└─┘  └──────────┘ 
typ    └────┘└────────────────────────┘└─┘ └──────────┘
doc    └────┘                          └─┘  └──────────┘ 
txt    └────┘                          └─┘               
par    └────┘                          └─┘               
pid                                   └─┘               
st   ──────────────────────────────────────────────────────┘└─
266    { rw finsupp.mem_supported,
id          └───────────────────┘
src      └─┘└───────────────────┘
typ      └─┘└───────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└──────────────────────┘└─
267      intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
268      have := finset.mem_coe.2 (finsupp.map_domain_support hx),
id               └────────────┘    └────────────────────────┘ └┘
src      └──────┘└────────────┘└─┘ └────────────────────────┘  
typ      └──────┘└────────────┘└─┘ └────────────────────────┘└┘
doc      └──────┘              └─┘                             
txt      └──────┘              └─┘                             
par      └──────┘              └─┘                             
pid      └───┘└─┘              └─┘                             
st   ───────────────────────────────────────────────────────────┘└─
269      rw finset.coe_image at this,
id          └──────────────┘
src      └─┘└──────────────┘└──────┘
typ      └─┘└──────────────┘└──────┘
doc      └─┘                └──────┘
txt      └─┘                └──────┘
par      └─┘                └──────┘
pid                        └──────┘
st   ──────────────────────────────┘└─
270      apply set.image_subset_range _ _ this, },
id             └────────────────────┘     └──┘
src      └────┘└────────────────────┘└───┘
typ      └────┘└────────────────────┘└───┘└──┘
doc      └────┘                      └───┘
txt      └────┘                      └───┘
par      └────┘                      └───┘
pid                                 └───┘
st   ────────────────────────────────────────┘└──┘
271    { rwa [finsupp.total_map_domain _ _ hv, left_id] }
id            └──────────────────────┘     └┘  └─────┘
src      └───┘└──────────────────────┘└───┘  └┘└─────┘└┘
typ      └───┘└──────────────────────┘└───┘└┘└┘└─────┘└┘
doc      └───┘                        └───┘  └┘       └┘
txt      └───┘                        └───┘  └┘       └┘
par      └───┘                        └───┘  └┘       └┘
pid         └┘                        └───┘  └┘       
st   ───────────────────────────────────────┘└───────┘└─
272  end
st   ──┘
273  
274  lemma linear_independent.restrict_of_comp_subtype {s : set ι}
id                                                          └─┘ 
src                                                         └─┘
typ                                                         └─┘ 
275    (hs : linear_independent R (v ∘ subtype.val : s → M)) :
id           └────────────────┘     └─────────┘      
src          └────────────────┘       └─────────┘
typ          └────────────────┘     └─────────┘      
doc          └────────────────┘
276    linear_independent R (function.restrict v s) :=
id     └────────────────┘   └───────────────┘  
src    └────────────────┘    └───────────────┘
typ    └────────────────┘   └───────────────┘  
doc    └────────────────┘
277  begin
st   └─────
278    have h_restrict : restrict v s = v ∘ (λ x, x.val) := rfl,
id                       └──────┘              └──┘     └─┘
src    └────────────────┘└──────┘     └──┘ └──┘└───┘└─┘
typ    └────────────────┘└──────┘   └──┘ └──┘└───┘└─┘
doc    └────────────────┘               └──┘     └───┘
txt    └────────────────┘               └──┘     └───┘
par    └────────────────┘               └──┘     └───┘
pid    └─────────────┘└─┘               └──┘     └──┘
st   ─────────────────────────────────────────────────────────┘└─
279    rw [linear_independent_iff, h_restrict, finsupp.total_comp],
id         └────────────────────┘  └────────┘  └────────────────┘
src    └──┘└────────────────────┘└┘          └┘└────────────────┘
typ    └──┘└────────────────────┘└┘└────────┘└┘└────────────────┘
doc    └──┘                      └┘          └┘                  
txt    └──┘                      └┘          └┘                  
par    └──┘                      └┘          └┘                  
pid      └┘                      └┘          └┘                  
st   ───────────────────────────┘└──────────┘└──────────────────┘└──
280    intros l hl,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
281    have h_map_domain_subtype_eq_0 : l.map_domain subtype.val = 0,
id                                      └──────────┘ └─────────┘
src    └───────────────────────────────┘└──────────┘└─────────┘ └┘
typ    └───────────────────────────────┘└──────────┘└─────────┘ └┘
doc    └───────────────────────────────┘└──────────┘            └┘
txt    └───────────────────────────────┘                        └┘
par    └───────────────────────────────┘                        └┘
pid    └────────────────────────────┘└─┘                        
st   ──────────────────────────────────────────────────────────────┘└─
282    { rw linear_independent_comp_subtype at hs,
id          └─────────────────────────────┘
src      └─┘└─────────────────────────────┘└────┘
typ      └─┘└─────────────────────────────┘└────┘
doc      └─┘                               └────┘
txt      └─┘                               └────┘
par      └─┘                               └────┘
pid                                       └────┘
st   ───┘└──────────────────────────────────────┘└─
283      apply hs (finsupp.lmap_domain R R (λ x : subtype s, x.val) l) _ hl,
id             └┘  └─────────────────┘           └─────┘              └┘
src      └────┘   └─────────────────┘    └───┘└─────┘ └┘     └┘ └──┘
typ      └────┘└┘ └─────────────────┘   └───┘└─────┘└┘     └┘└──┘└┘
doc      └────┘                          └───┘        └┘     └┘ └──┘
txt      └────┘                          └───┘        └┘     └┘ └──┘
par      └────┘                          └───┘        └┘     └┘ └──┘
pid                                     └───┘        └┘     └┘ └──┘
st   ─────────────────────────────────────────────────────────────────────┘└─
284      rw finsupp.mem_supported,
id          └───────────────────┘
src      └─┘└───────────────────┘
typ      └─┘└───────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────────┘└─
285      simp,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
286      intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
287      have := finset.mem_coe.2 (finsupp.map_domain_support (finset.mem_coe.1 hx)),
id                                 └────────────────────────┘  └────────────┘   └┘
src      └──────┘              └─┘ └────────────────────────┘ └────────────┘└─┘  └┘
typ      └──────┘              └─┘ └────────────────────────┘ └────────────┘└─┘└┘└┘
doc      └──────┘              └─┘                                          └─┘  └┘
txt      └──────┘              └─┘                                          └─┘  └┘
par      └──────┘              └─┘                                          └─┘  └┘
pid      └───┘└─┘              └─┘                                          └─┘  └┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
288      rw finset.coe_image at this,
id          └──────────────┘
src      └─┘└──────────────┘└──────┘
typ      └─┘└──────────────┘└──────┘
doc      └─┘                └──────┘
txt      └─┘                └──────┘
par      └─┘                └──────┘
pid                        └──────┘
st   ──────────────────────────────┘└─
289      exact subtype.val_image_subset _ _ this },
id             └──────────────────────┘     └──┘
src      └────┘└──────────────────────┘└───┘    
typ      └────┘└──────────────────────┘└───┘└──┘
doc      └────┘                        └───┘    
txt      └────┘                        └───┘    
par      └────┘                        └───┘    
pid                                   └───┘    
st   ───────────────────────────────────────────┘└┘
290    apply @finsupp.injective_map_domain _ (subtype s) ι,
id            └──────────────────────────┘    └─────┘   
src    └────┘ └──────────────────────────┘└─┘ └─────┘ └┘
typ    └────┘ └──────────────────────────┘└─┘ └─────┘└┘
doc    └────┘                             └─┘         └┘
txt    └────┘                             └─┘         └┘
par    └────┘                             └─┘         └┘
pid                                      └─┘         └┘
st   ────────────────────────────────────────────────────┘└─
291    { apply subtype.val_injective },
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘                     
txt      └────┘                     
par      └────┘                     
pid                                
st   ───┘└──────────────────────────┘└┘
292    { simpa },
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────┘└──
293  end
st   ──┘
294  
295  lemma linear_independent_empty : linear_independent R (λ x, x : (∅ : set M) → M) :=
id                                    └────────────────┘             └─┘     
src                                   └────────────────┘                 └─┘
typ                                   └────────────────┘             └─┘     
doc                                   └────────────────┘
296  by simp [linear_independent_subtype_disjoint]
id            └─────────────────────────────────┘
src     └────┘└─────────────────────────────────┘└─
typ     └────┘└─────────────────────────────────┘└─
doc     └────┘                                   └─
txt     └────┘                                   └─
par     └────┘                                   └─
pid                                            
st     └───────────────────────────────────────────
297  
src  
typ  
doc  
txt  
par  
pid  
st   
298  lemma linear_independent.mono {t s : set M} (h : t ⊆ s) :
id                                        └─┘          
src                                       └─┘           
typ                                       └─┘          
299    linear_independent R (λ x, x : s → M) → linear_independent R (λ x, x : t → M) :=
id     └────────────────┘                 └────────────────┘             
src    └────────────────┘                      └────────────────┘
typ    └────────────────┘                 └────────────────┘             
doc    └────────────────┘                      └────────────────┘
300  begin
st   └─────
301   simp only [linear_independent_subtype_disjoint],
id               └─────────────────────────────────┘
src   └─────────┘└─────────────────────────────────┘
typ   └─────────┘└─────────────────────────────────┘
doc   └─────────┘                                   
txt   └─────────┘                                   
par   └─────────┘                                   
pid       └──┘└┘                                   
st   ───────────────────────────────────────────────┘└─
302   exact (disjoint_mono_left (finsupp.supported_mono h))
id           └────────────────┘  └────────────────────┘ 
src   └────┘ └────────────────┘ └────────────────────┘ └─┘
typ   └────┘ └────────────────┘ └────────────────────┘└─┘
doc   └────┘                                           └─┘
txt   └────┘                                           └─┘
par   └────┘                                           └─┘
pid                                                   └┘
st   ──────────────────────────────────────────────────────┘
303  end
st   └─┘
304  
305  lemma linear_independent_union {s t : set M}
id                                         └─┘ 
src                                        └─┘
typ                                        └─┘ 
306    (hs : linear_independent R (λ x, x : s → M)) (ht : linear_independent R (λ x, x : t → M))
id           └────────────────┘                      └────────────────┘             
src          └────────────────┘                           └────────────────┘
typ          └────────────────┘                      └────────────────┘             
doc          └────────────────┘                           └────────────────┘
307    (hst : disjoint (span R s) (span R t)) :
id            └──────┘  └──┘     └──┘  
src           └──────┘  └──┘       └──┘
typ           └──────┘  └──┘     └──┘  
doc           └──────┘  └──┘       └──┘
308    linear_independent R (λ x, x : (s ∪ t) → M) :=
id     └────────────────┘                 
src    └────────────────┘                
typ    └────────────────┘                 
doc    └────────────────┘
309  begin
st   └─────
310    rw [linear_independent_subtype_disjoint, disjoint_def, finsupp.supported_union],
id         └─────────────────────────────────┘  └──────────┘  └─────────────────────┘
src    └──┘└─────────────────────────────────┘└┘└──────────┘└┘└─────────────────────┘
typ    └──┘└─────────────────────────────────┘└┘└──────────┘└┘└─────────────────────┘
doc    └──┘                                   └┘            └┘                       
txt    └──┘                                   └┘            └┘                       
par    └──┘                                   └┘            └┘                       
pid      └┘                                   └┘            └┘                       
st   ────────────────────────────────────────┘└────────────┘└───────────────────────┘└──
311    intros l h₁ h₂, rw mem_sup at h₁,
id                        └─────┘
src    └────────────┘  └─┘└─────┘└────┘
typ    └────────────┘  └─┘└─────┘└────┘
doc    └────────────┘  └─┘       └────┘
txt    └────────────┘  └─┘       └────┘
par    └────────────┘  └─┘       └────┘
pid          └──────┘           └────┘
st   ───────────────┘└────────────────┘└─
312    rcases h₁ with ⟨ls, hls, lt, hlt, rfl⟩,
id            └┘
src    └─────┘  └───────────────────────────┘
typ    └─────┘└┘└───────────────────────────┘
doc    └─────┘  └───────────────────────────┘
txt    └─────┘  └───────────────────────────┘
par    └─────┘  └───────────────────────────┘
pid            └───────────────────────────┘
st   ───────────────────────────────────────┘└─
313    have h_ls_mem_t : finsupp.total M M R id ls ∈ span R t,
id                       └───────────┘      └┘ └┘  └──┘  
src    └────────────────┘└───────────┘   └┘  └──┘ 
typ    └────────────────┘└───────────┘  └┘└┘└──┘
doc    └────────────────┘└───────────┘        └──┘ 
txt    └────────────────┘                          
par    └────────────────┘                          
pid    └─────────────┘└─┘                          
st   ───────────────────────────────────────────────────────┘└─
314    { rw [← image_id t, finsupp.span_eq_map_total],
id             └──────┘   └───────────────────────┘
src      └────┘└──────┘ └┘└───────────────────────┘
typ      └────┘└──────┘└┘└───────────────────────┘
doc      └────┘         └┘                         
txt      └────┘         └┘                         
par      └────┘         └┘                         
pid        └──┘         └┘                         
st   ───┘└──────────────┘└─────────────────────────┘└──
315      apply (add_mem_iff_left (map _ _) (mem_image_of_mem _ hlt)).1,
id              └──────────────┘  └─┘       └──────────────┘   └─┘
src      └────┘ └──────────────┘ └─┘└────┘ └──────────────┘└─┘   └──┘
typ      └────┘ └──────────────┘ └─┘└────┘ └──────────────┘└─┘└─┘└──┘
doc      └────┘                  └─┘└────┘                 └─┘   └──┘
txt      └────┘                     └────┘                 └─┘   └──┘
par      └────┘                     └────┘                 └─┘   └──┘
pid                                └────┘                 └─┘   └┘└┘
st   ────────────────────────────────────────────────────────────────┘└─
316      rw [← linear_map.map_add, linear_map.mem_ker.1 h₂],
id             └────────────────┘  └────────────────┘   └┘
src      └────┘└────────────────┘└┘└────────────────┘└─┘  
typ      └────┘└────────────────┘└┘└────────────────┘└─┘└┘
doc      └────┘                  └┘                  └─┘  
txt      └────┘                  └┘                  └─┘  
par      └────┘                  └┘                  └─┘  
pid        └──┘                  └┘                  └─┘  
st   ───────────────────────────┘└───────────────────────┘└──
317      apply zero_mem },
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ──────────────────┘└┘
318    have h_lt_mem_s : finsupp.total M M R id lt ∈ span R s,
id                       └───────────┘      └┘ └┘   └──┘  
src    └────────────────┘└───────────┘   └┘   └──┘ 
typ    └────────────────┘└───────────┘  └┘└┘ └──┘
doc    └────────────────┘└───────────┘        └──┘ 
txt    └────────────────┘                          
par    └────────────────┘                          
pid    └─────────────┘└─┘                          
st   ───────────────────────────────────────────────────────┘└─
319    { rw [← image_id s, finsupp.span_eq_map_total],
id             └──────┘   └───────────────────────┘
src      └────┘└──────┘ └┘└───────────────────────┘
typ      └────┘└──────┘└┘└───────────────────────┘
doc      └────┘         └┘                         
txt      └────┘         └┘                         
par      └────┘         └┘                         
pid        └──┘         └┘                         
st   ───┘└──────────────┘└─────────────────────────┘└──
320      apply (add_mem_iff_left (map _ _) (mem_image_of_mem _ hls)).1,
id              └──────────────┘  └─┘       └──────────────┘   └─┘
src      └────┘ └──────────────┘ └─┘└────┘ └──────────────┘└─┘   └──┘
typ      └────┘ └──────────────┘ └─┘└────┘ └──────────────┘└─┘└─┘└──┘
doc      └────┘                  └─┘└────┘                 └─┘   └──┘
txt      └────┘                     └────┘                 └─┘   └──┘
par      └────┘                     └────┘                 └─┘   └──┘
pid                                └────┘                 └─┘   └┘└┘
st   ────────────────────────────────────────────────────────────────┘└─
321      rw [← linear_map.map_add, add_comm, linear_map.mem_ker.1 h₂],
id             └────────────────┘  └──────┘  └────────────────┘   └┘
src      └────┘└────────────────┘└┘└──────┘└┘└────────────────┘└─┘  
typ      └────┘└────────────────┘└┘└──────┘└┘└────────────────┘└─┘└┘
doc      └────┘                  └┘        └┘                  └─┘  
txt      └────┘                  └┘        └┘                  └─┘  
par      └────┘                  └┘        └┘                  └─┘  
pid        └──┘                  └┘        └┘                  └─┘  
st   ───────────────────────────┘└────────┘└───────────────────────┘└──
322      apply zero_mem },
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ──────────────────┘└┘
323    have h_ls_mem_s : (finsupp.total M M R id) ls ∈ span R s,
id                        └───────────┘      └┘  └┘   └──┘  
src    └────────────────┘ └───────────┘   └┘└┘   └──┘ 
typ    └────────────────┘ └───────────┘  └┘└┘└┘ └──┘
doc    └────────────────┘ └───────────┘     └┘   └──┘ 
txt    └────────────────┘                   └┘        
par    └────────────────┘                   └┘        
pid    └─────────────┘└─┘                   └┘        
st   ─────────────────────────────────────────────────────────┘└─
324    { rw ← image_id s,
id            └──────┘ 
src      └───┘└──────┘
typ      └───┘└──────┘
doc      └───┘        
txt      └───┘        
par      └───┘        
pid        └─┘        
st   ───┘└─────────────┘└─
325      apply (finsupp.mem_span_iff_total _).2 ⟨ls, hls, rfl⟩ },
id              └────────────────────────┘       └┘  └─┘  └─┘
src      └────┘ └────────────────────────┘└────┘   └┘   └┘└─┘└┘
typ      └────┘ └────────────────────────┘└────┘ └┘└┘└─┘└┘└─┘└┘
doc      └────┘                           └────┘   └┘   └┘   └┘
txt      └────┘                           └────┘   └┘   └┘   └┘
par      └────┘                           └────┘   └┘   └┘   └┘
pid                                      └────┘   └┘   └┘   
st   ─────────────────────────────────────────────────────────┘└┘
326    have h_lt_mem_t : (finsupp.total M M R id) lt ∈ span R t,
id                        └───────────┘      └┘  └┘   └──┘  
src    └────────────────┘ └───────────┘   └┘└┘   └──┘ 
typ    └────────────────┘ └───────────┘  └┘└┘└┘ └──┘
doc    └────────────────┘ └───────────┘     └┘   └──┘ 
txt    └────────────────┘                   └┘        
par    └────────────────┘                   └┘        
pid    └─────────────┘└─┘                   └┘        
st   ─────────────────────────────────────────────────────────┘└─
327    { rw ← image_id t,
id            └──────┘ 
src      └───┘└──────┘
typ      └───┘└──────┘
doc      └───┘        
txt      └───┘        
par      └───┘        
pid        └─┘        
st   ───┘└─────────────┘└─
328      apply (finsupp.mem_span_iff_total _).2 ⟨lt, hlt, rfl⟩ },
id              └────────────────────────┘       └┘  └─┘  └─┘
src      └────┘ └────────────────────────┘└────┘   └┘   └┘└─┘└┘
typ      └────┘ └────────────────────────┘└────┘ └┘└┘└─┘└┘└─┘└┘
doc      └────┘                           └────┘   └┘   └┘   └┘
txt      └────┘                           └────┘   └┘   └┘   └┘
par      └────┘                           └────┘   └┘   └┘   └┘
pid                                      └────┘   └┘   └┘   
st   ─────────────────────────────────────────────────────────┘└┘
329    have h_ls_0 : ls = 0 :=
id                   └┘ 
src    └────────────┘  └─────
typ    └────────────┘└┘└─────
doc    └────────────┘   └─────
txt    └────────────┘   └─────
par    └────────────┘   └─────
pid    └─────────┘└─┘   └────
st   ──────────────────────────
330      disjoint_def.1 (linear_independent_subtype_disjoint.1 hs) _ hls
id                       └─────────────────────────────────┘   └┘    └─┘
src  ───┘            └─┘ └─────────────────────────────────┘└─┘  └──┘   
typ  ───┘            └─┘ └─────────────────────────────────┘└─┘└┘└──┘└─┘
doc  ───┘            └─┘                                    └─┘  └──┘   
txt  ───┘            └─┘                                    └─┘  └──┘   
par  ───┘            └─┘                                    └─┘  └──┘   
pid  ───┘            └─┘                                    └─┘  └──┘   
st   ────────────────────────────────────────────────────────────────────
331      (linear_map.mem_ker.2 $ disjoint_def.1 hst (finsupp.total M M R id ls) h_ls_mem_s h_ls_mem_t),
id        └────────────────┘     └──────────┘   └─┘  └───────────┘     └┘ └┘  └────────┘ └────────┘
src  ───┘ └────────────────┘└─┘ └──────────┘└─┘    └───────────┘   └┘  └┘                    
typ  ───┘ └────────────────┘└─┘ └──────────┘└─┘└─┘ └───────────┘ └┘└┘└┘└────────┘└────────┘
doc  ───┘                   └─┘             └─┘    └───────────┘       └┘                    
txt  ───┘                   └─┘             └─┘                        └┘                    
par  ───┘                   └─┘             └─┘                        └┘                    
pid  ───┘                   └─┘             └─┘                        └┘                    
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
332    have h_lt_0 : lt = 0 :=
id                   └┘
src    └────────────┘   └─────
typ    └────────────┘└┘ └─────
doc    └────────────┘   └─────
txt    └────────────┘   └─────
par    └────────────┘   └─────
pid    └─────────┘└─┘   └────
st   ──────────────────────────
333      disjoint_def.1 (linear_independent_subtype_disjoint.1 ht) _ hlt
id                       └─────────────────────────────────┘   └┘    └─┘
src  ───┘            └─┘ └─────────────────────────────────┘└─┘  └──┘   
typ  ───┘            └─┘ └─────────────────────────────────┘└─┘└┘└──┘└─┘
doc  ───┘            └─┘                                    └─┘  └──┘   
txt  ───┘            └─┘                                    └─┘  └──┘   
par  ───┘            └─┘                                    └─┘  └──┘   
pid  ───┘            └─┘                                    └─┘  └──┘   
st   ────────────────────────────────────────────────────────────────────
334      (linear_map.mem_ker.2 $ disjoint_def.1 hst (finsupp.total M M R id lt) h_lt_mem_s h_lt_mem_t),
id        └────────────────┘     └──────────┘   └─┘  └───────────┘     └┘ └┘  └────────┘ └────────┘
src  ───┘ └────────────────┘└─┘ └──────────┘└─┘    └───────────┘   └┘  └┘                    
typ  ───┘ └────────────────┘└─┘ └──────────┘└─┘└─┘ └───────────┘ └┘└┘└┘└────────┘└────────┘
doc  ───┘                   └─┘             └─┘    └───────────┘       └┘                    
txt  ───┘                   └─┘             └─┘                        └┘                    
par  ───┘                   └─┘             └─┘                        └┘                    
pid  ───┘                   └─┘             └─┘                        └┘                    
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
335    show ls + lt = 0,
id          └┘  └┘
src    └───┘     └┘
typ    └───┘└┘└┘ └┘
doc    └───┘      └┘
txt    └───┘      └┘
par    └───┘      └┘
pid    └───┘      
st   ─────────────────┘
336      by simp [h_ls_0, h_lt_0],
id                └────┘  └────┘
src         └────┘      └┘      
typ         └────┘└────┘└┘└────┘
doc         └────┘      └┘      
txt         └────┘      └┘      
par         └────┘      └┘      
pid                   └┘      
st                               └─
337  end
st   ──┘
338  
339  lemma linear_independent_of_finite (s : set M)
id                                           └─┘ 
src                                          └─┘
typ                                          └─┘ 
340    (H : ∀ t ⊆ s, finite t → linear_independent R (λ x, x : t → M)) :
id                 └────┘    └────────────────┘             
src                 └────┘     └────────────────┘
typ                └────┘    └────────────────┘             
doc                  └────┘     └────────────────┘
341    linear_independent R (λ x, x : s → M) :=
id     └────────────────┘             
src    └────────────────┘
typ    └────────────────┘             
doc    └────────────────┘
342  linear_independent_subtype.2 $
id   └────────────────────────┘
src  └────────────────────────┘
typ  └────────────────────────┘
343    λ l hl, linear_independent_subtype.1 (H _ hl (finset.finite_to_set _)) l (subset.refl _)
id        └┘  └────────────────────────┘      └┘  └──────────────────┘       └─────────┘
src            └────────────────────────┘           └──────────────────┘        └─────────┘
typ       └┘  └────────────────────────┘      └┘  └──────────────────┘       └─────────┘
344  
345  lemma linear_independent_Union_of_directed {η : Type*}
346    {s : η → set M} (hs : directed (⊆) s)
id             └─┘         └──────┘    
src             └─┘          └──────┘ 
typ            └─┘         └──────┘    
doc                          └──────┘
347    (h : ∀ i, linear_independent R (λ x, x : s i → M)) :
id              └────────────────┘              
src              └────────────────┘
typ             └────────────────┘              
doc              └────────────────┘
348    linear_independent R (λ x, x : (⋃ i, s i) → M) :=
id     └────────────────┘                  
src    └────────────────┘                
typ    └────────────────┘                  
doc    └────────────────┘                
349  begin
st   └─────
350    haveI := classical.dec (nonempty η),
id              └───────────┘  └──────┘ 
src    └───────┘└───────────┘ └──────┘ 
typ    └───────┘└───────────┘ └──────┘
doc    └───────┘                       
txt    └───────┘                       
par    └───────┘                       
pid         └─┘                       
st   ────────────────────────────────────┘└─
351    by_cases hη : nonempty η,
id                   └──────┘ 
src    └───────┘  └─┘└──────┘
typ    └───────┘  └─┘└──────┘
doc    └───────┘  └─┘        
txt    └───────┘  └─┘        
par    └───────┘  └─┘        
pid              └─┘        
st   ─────────────────────────┘└─
352    { refine linear_independent_of_finite (⋃ i, s i) (λ t ht ft, _),
id              └──────────────────────────┘     
src      └─────┘└──────────────────────────┘ └┘  └┘  └──────────┘
typ      └─────┘└──────────────────────────┘ └┘ └┘  └──────────┘
doc      └─────┘                             └┘  └┘  └──────────┘
txt      └─────┘                              └┘   └┘  └──────────┘
par      └─────┘                              └┘   └┘  └──────────┘
pid                                          └┘   └┘  └──────────┘
st   ───┘└───────────────────────────────────────────────────────────┘└─
353      rcases finite_subset_Union ft ht with ⟨I, fi, hI⟩,
id              └─────────────────┘ └┘ └┘
src      └─────┘└─────────────────┘    └───────────────┘
typ      └─────┘└─────────────────┘└┘└┘└───────────────┘
doc      └─────┘                       └───────────────┘
txt      └─────┘                       └───────────────┘
par      └─────┘                       └───────────────┘
pid                                   └───────────────┘
st   ────────────────────────────────────────────────────┘└─
354      rcases hs.finset_le hη fi.to_finset with ⟨i, hi⟩,
id              └──────────┘ └┘ └──────────┘
src      └─────┘└──────────┘  └──────────┘└───────────┘
typ      └─────┘└──────────┘└┘└──────────┘└───────────┘
doc      └─────┘              └──────────┘└───────────┘
txt      └─────┘                          └───────────┘
par      └─────┘                          └───────────┘
pid                                      └───────────┘
st   ───────────────────────────────────────────────────┘└─
355      exact (h i).mono (subset.trans hI $ bUnion_subset $
id                       └──────────┘ └┘   └───────────┘
src      └────┘   └─────┘ └──────────┘   └───────────┘ 
typ      └────┘ └─────┘ └──────────┘└┘ └───────────┘ 
doc      └────┘   └─────┘                              
txt      └────┘   └─────┘                              
par      └────┘   └─────┘                              
pid              └─────┘                              
st   ────────────────────────────────────────────────────────
356        λ j hj, hi j (finite.mem_to_finset.2 hj)) },
id                 └┘    └──────────────────┘
src  ─────┘ └─────┘    └──────────────────┘└─┘  └─┘
typ  ─────┘ └─────┘└┘  └──────────────────┘└─┘  └─┘
doc  ─────┘ └─────┘                        └─┘  └─┘
txt  ─────┘ └─────┘                        └─┘  └─┘
par  ─────┘ └─────┘                        └─┘  └─┘
pid  ─────┘ └─────┘                        └─┘  └┘
st   ───────────────────────────────────────────────┘└┘
357    { refine linear_independent_empty.mono _,
id              └───────────────────────────┘
src      └─────┘└───────────────────────────┘└┘
typ      └─────┘└───────────────────────────┘└┘
doc      └─────┘                             └┘
txt      └─────┘                             └┘
par      └─────┘                             └┘
pid                                         └┘
st   ─────────────────────────────────────────┘└─
358      rintro _ ⟨_, ⟨i, _⟩, _⟩, exact hη ⟨i⟩ }
id                                      └┘  
src      └─────────────────────┘  └────┘    └┘
typ      └─────────────────────┘  └────┘└┘ └┘
doc      └─────────────────────┘  └────┘    └┘
txt      └─────────────────────┘  └────┘    └┘
par      └─────────────────────┘  └────┘    └┘
pid            └───────────────┘           
st   ──────────────────────────┘└─────────────┘└─
359  end
st   ──┘
360  
361  lemma linear_independent_sUnion_of_directed {s : set (set M)}
id                                                    └─┘  └─┘ 
src                                                   └─┘  └─┘
typ                                                   └─┘  └─┘ 
362    (hs : directed_on (⊆) s)
id           └─────────┘    
src          └─────────┘ 
typ          └─────────┘    
doc          └─────────┘
363    (h : ∀ a ∈ s, linear_independent R (λ x, x : (a : set M) → M)) :
id                 └────────────────┘          └┘   └─┘     
src                  └────────────────┘                  └─┘
typ                └────────────────┘             └─┘     
doc                  └────────────────┘
364    linear_independent R (λ x, x : (⋃₀ s) → M) :=
id     └────────────────┘           └┘     
src    └────────────────┘              └┘
typ    └────────────────┘           └┘     
doc    └────────────────┘
365  by rw sUnion_eq_Union; exact
id         └─────────────┘
src     └─┘└─────────────┘  └────┘
typ     └─┘└─────────────┘  └────┘
doc     └─┘                 └────┘
txt     └─┘                 └────┘
par     └─┘                 └────┘
pid                             
st     └──────────────────────────
366  linear_independent_Union_of_directed
id   └──────────────────────────────────┘
src  └──────────────────────────────────┘
typ  └──────────────────────────────────┘
doc                                      
txt                                      
par                                      
pid                                      
st   ─────────────────────────────────────
367    ((directed_on_iff_directed _).1 hs) (by simpa using h)
id       └──────────────────────┘      └┘                  
src  ─┘  └──────────────────────┘└────┘  └┘   └──────────┘ └─
typ  ─┘  └──────────────────────┘└────┘└┘└┘   └──────────┘└─
doc  ─┘                          └────┘  └┘   └──────────┘ └─
txt  ─┘                          └────┘  └┘   └──────────┘ └─
par  ─┘                          └────┘  └┘   └──────────┘ └─
pid  ─┘                          └────┘  └┘   └───────────┘ 
st   ────────────────────────────────────────┘└────────────┘└─
368  
src  
typ  
doc  
txt  
par  
pid  
st   
369  lemma linear_independent_bUnion_of_directed {η} {s : set η} {t : η → set M}
id                                                        └─┘           └─┘ 
src                                                       └─┘             └─┘
typ                                                       └─┘           └─┘ 
370    (hs : directed_on (t ⁻¹'o (⊆)) s) (h : ∀a∈s, linear_independent R (λ x, x : t a → M)) :
id           └─────────┘   └──┘                └────────────────┘              
src          └─────────┘    └──┘                   └────────────────┘
typ          └─────────┘   └──┘                └────────────────┘              
doc          └─────────┘    └──┘                    └────────────────┘
371    linear_independent R (λ x, x : (⋃a∈s, t a) → M) :=
id     └────────────────┘                  
src    └────────────────┘                 
typ    └────────────────┘                  
doc    └────────────────┘                 
372  by rw bUnion_eq_Union; exact
id         └─────────────┘
src     └─┘└─────────────┘  └────┘
typ     └─┘└─────────────┘  └────┘
doc     └─┘                 └────┘
txt     └─┘                 └────┘
par     └─┘                 └────┘
pid                             
st     └──────────────────────────
373  linear_independent_Union_of_directed
id   └──────────────────────────────────┘
src  └──────────────────────────────────┘
typ  └──────────────────────────────────┘
doc                                      
txt                                      
par                                      
pid                                      
st   ─────────────────────────────────────
374    ((directed_comp _ _ _).2 $ (directed_on_iff_directed _).1 hs)
id       └───────────┘             └──────────────────────┘      └┘
src  ─┘  └───────────┘└────────┘  └──────────────────────┘└────┘  └─
typ  ─┘  └───────────┘└────────┘  └──────────────────────┘└────┘└┘└─
doc  ─┘               └────────┘                          └────┘  └─
txt  ─┘               └────────┘                          └────┘  └─
par  ─┘               └────────┘                          └────┘  └─
pid  ─┘               └────────┘                          └────┘  └─
st   ────────────────────────────────────────────────────────────────
375    (by simpa using h)
id                     
src  ─┘   └──────────┘ └─
typ  ─┘   └──────────┘└─
doc  ─┘   └──────────┘ └─
txt  ─┘   └──────────┘ └─
par  ─┘   └──────────┘ └─
pid  ─┘   └───────────┘ 
st   ────┘└────────────┘└─
376  
src  
typ  
doc  
txt  
par  
pid  
st   
377  lemma linear_independent_Union_finite_subtype {ι : Type*} {f : ι → set M}
id                                                                     └─┘ 
src                                                                     └─┘
typ                                                                    └─┘ 
378    (hl : ∀i, linear_independent R (λ x, x : f i → M))
id              └────────────────┘              
src              └────────────────┘
typ             └────────────────┘              
doc              └────────────────┘
379    (hd : ∀i, ∀t:set ι, finite t → i ∉ t → disjoint (span R (f i)) (⨆i∈t, span R (f i))) :
id                 └─┘   └────┘         └──────┘  └──┘          └──┘    
src                 └─┘    └────┘            └──────┘  └──┘               └──┘
typ                └─┘   └────┘         └──────┘  └──┘          └──┘    
doc                        └────┘             └──────┘  └──┘               └──┘
380    linear_independent R (λ x, x : (⋃i, f i) → M) :=
id     └────────────────┘                 
src    └────────────────┘               
typ    └────────────────┘                 
doc    └────────────────┘               
381  begin
st   └─────
382    rw [Union_eq_Union_finset f],
id         └───────────────────┘ 
src    └──┘└───────────────────┘ 
typ    └──┘└───────────────────┘
doc    └──┘                      
txt    └──┘                      
par    └──┘                      
pid      └┘                      
st   ────────────────────────────┘└──
383    apply linear_independent_Union_of_directed,
id           └──────────────────────────────────┘
src    └────┘└──────────────────────────────────┘
typ    └────┘└──────────────────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────────────────────┘└─
384    apply directed_of_sup,
id           └─────────────┘
src    └────┘└─────────────┘
typ    └────┘└─────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────┘└─
385    exact (assume t₁ t₂ ht, Union_subset_Union $ assume i, Union_subset_Union_const $ assume h, ht h),
id                             └────────────────┘             └──────────────────────┘
src    └────┘       └─────────┘└────────────────┘       └──┘└──────────────────────┘       └──┘   
typ    └────┘       └─────────┘└────────────────┘       └──┘└──────────────────────┘       └──┘   
doc    └────┘       └─────────┘                         └──┘                               └──┘   
txt    └────┘       └─────────┘                         └──┘                               └──┘   
par    └────┘       └─────────┘                         └──┘                               └──┘   
pid                └─────────┘                         └──┘                               └──┘   
st   ──────────────────────────────────────────────────────────────────────────────────────────────────┘└─
386    assume t, rw [set.Union, ← finset.sup_eq_supr],
id                   └───────┘    └────────────────┘
src    └──────┘  └──┘└───────┘└──┘└────────────────┘
typ    └──────┘  └──┘└───────┘└──┘└────────────────┘
doc    └──────┘  └──┘└───────┘└──┘                  
txt    └──────┘  └──┘         └──┘                  
par    └──────┘  └──┘         └──┘                  
pid    └──────┘    └┘         └──┘                  
st   ─────────┘└─────────────┘└────────────────────┘└──
387    refine t.induction_on _ _,
id            └────────────┘
src    └─────┘└────────────┘└──┘
typ    └─────┘└────────────┘└──┘
doc    └─────┘└────────────┘└──┘
txt    └─────┘              └──┘
par    └─────┘              └──┘
pid                        └──┘
st   ──────────────────────────┘└─
388    { rw finset.sup_empty,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└─────────────────┘└─
389      apply linear_independent_empty_type (not_nonempty_iff_imp_false.2 _),
id             └───────────────────────────┘  └────────────────────────┘
src      └────┘└───────────────────────────┘ └────────────────────────┘└───┘
typ      └────┘└───────────────────────────┘ └────────────────────────┘└───┘
doc      └────┘                                                        └───┘
txt      └────┘                                                        └───┘
par      └────┘                                                        └───┘
pid                                                                   └───┘
st   ───────────────────────────────────────────────────────────────────────┘└─
390      exact λ x, set.not_mem_empty x (subtype.mem x) },
id                  └───────────────┘    └─────────┘
src      └────┘ └──┘└───────────────┘  └─────────┘ └┘
typ      └────┘ └──┘└───────────────┘  └─────────┘ └┘
doc      └────┘ └──┘                               └┘
txt      └────┘ └──┘                               └┘
par      └────┘ └──┘                               └┘
pid            └──┘                               
st   ──────────────────────────────────────────────────┘└┘
391    { rintros ⟨i⟩ s his ih,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid             └───────────┘
st   ───────────────────────┘└─
392      rw [finset.sup_insert],
id           └───────────────┘
src      └──┘└───────────────┘
typ      └──┘└───────────────┘
doc      └──┘                 
txt      └──┘                 
par      └──┘                 
pid        └┘                 
st   ────────────────────────┘
393      apply linear_independent_union,
394      { apply hl },
st                  └┘
395      { apply ih },
st                  └┘
396      rw [finset.sup_eq_supr],
397      refine disjoint_mono (le_refl _) _ (hd i _ _ his),
id                                                     
src                                                      
typ                                                    
doc                                                      
txt                                                      
par                                                      
pid                                                      
st                                                      └┘
398      { simp only [(span_Union _).symm],
id                              
src                             
typ                             
399        refine span_mono (@supr_le_supr2 (set M) _ _ _ _ _ _),
id                                   
src                                 
typ                                  
400        rintros ⟨i⟩, exact ⟨i, le_refl _⟩ },
id                                   
src                                  
typ                                  
st                                           └┘
401      { change finite (plift.up ⁻¹' s.to_set),
id                               
src                              
typ                              
doc                                  
402        exact finite_preimage (inj_on_of_injective _ (assume i j, plift.up.inj))
id                                                      
src                                                       
typ                                                     
403          s.finite_to_set } }
id                  
src                 
typ                 
st                           └───
404  end
st   ──┘
405  
406  lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*}
id                                                           
typ                                                          
407    {f : Π j : η, ιs j → M}
id                  └┘    
typ                 └┘    
408    (hindep : ∀j, linear_independent R (f j))
id                  └────────────────┘    
src                  └────────────────┘
typ                 └────────────────┘    
doc                  └────────────────┘
409    (hd : ∀i, ∀t:set η, finite t → i ∉ t →
id                 └─┘   └────┘      
src                 └─┘    └────┘       
typ                └─┘   └────┘      
doc                        └────┘
410        disjoint (span R (range (f i))) (⨆i∈t, span R (range (f i)))) :
id         └──────┘  └──┘   └───┘          └──┘   └───┘   
src        └──────┘  └──┘    └───┘              └──┘    └───┘
typ        └──────┘  └──┘   └───┘          └──┘   └───┘   
doc        └──────┘  └──┘    └───┘              └──┘    └───┘
411    linear_independent R (λ ji : Σ j, ιs j, f ji.1 ji.2) :=
id     └────────────────┘            └┘    └┘  └┘
src    └────────────────┘                            
typ    └────────────────┘            └┘    └┘  └┘
doc    └────────────────┘
412  begin
st   └─────
413    by_cases zero_eq_one : (0 : R) = 1,
id                                   
src    └───────┘           └─┘ └──┘ └┘└┘
typ    └───────┘           └─┘ └──┘└┘└┘
doc    └───────┘           └─┘ └──┘ └┘ └┘
txt    └───────┘           └─┘ └──┘ └┘ └┘
par    └───────┘           └─┘ └──┘ └┘ └┘
pid                       └─┘ └──┘ └┘ 
st   ───────────────────────────────────┘
414    { apply linear_independent_of_zero_eq_one zero_eq_one },
st                                                           
415    apply linear_independent.of_subtype_range,
416    { rintros ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy,
417      by_cases h_cases : x₁ = y₁,
418      subst h_cases,
419      { apply sigma.eq,
420        rw linear_independent.injective zero_eq_one (hindep _) hxy,
421        refl },
st              
422      { have h0 : f x₁ x₂ = 0,
423        { apply disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁)
424            (λ h, h_cases (eq_of_mem_singleton h))) (f x₁ x₂) (subset_span (mem_range_self _)),
425          rw supr_singleton,
426          simp only [] at hxy,
427          rw hxy,
428          exact (subset_span (mem_range_self y₂)) },
st                                                   
429        exact false.elim (ne_zero_of_linear_independent zero_eq_one (hindep x₁) h0) } },
st                                                                                     └─┘
430    rw range_sigma_eq_Union_range,
431    apply linear_independent_Union_finite_subtype (λ j, (hindep j).to_subtype_range) hd,
st                                                                                        └─
432  end
st   ──┘
433  
434  end subtype
435  
436  section repr
437  variables (hv : linear_independent R v)
id                   └────────────────┘
src                  └────────────────┘
typ                  └────────────────┘
doc                  └────────────────┘
438  
439  /-- Canonical isomorphism between linear combinations and the span of linearly independent vectors. -/
440  def linear_independent.total_equiv (hv : linear_independent R v) : (ι →₀ R) ≃ₗ[R] span R (range v) :=
id                                            └────────────────┘        └┘   └─┘ └──┘   └───┘ 
src                                           └────────────────┘           └┘    └─┘  └──┘    └───┘
typ                                           └────────────────┘        └┘   └─┘ └──┘   └───┘ 
doc                                           └────────────────┘           └┘    └─┘  └──┘    └───┘
441  begin
st   └───┘
442  apply linear_equiv.of_bijective (linear_map.cod_restrict (span R (range v)) (finsupp.total ι M R v) _),
443  { rw linear_map.ker_cod_restrict,
444    apply hv },
st              └┘
445  { rw [linear_map.range, linear_map.map_cod_restrict, ← linear_map.range_le_iff_comap,
446    range_subtype, map_top],
447    rw finsupp.range_total,
448    apply le_refl (span R (range v)) },
id                                 
typ                                
st                                      └┘
449  { intro l,
450    rw ← finsupp.range_total,
451    rw linear_map.mem_range,
452    apply mem_range_self l }
st                            └─
453  end
st   ──┘
454  
455  /-- Linear combination representing a vector in the span of linearly independent vectors.
456  
457     Given a family of linearly independent vectors, we can represent any vector in their span as
458     a linear combination of these vectors. These are provided by this linear map.
459     It is simply one direction of `linear_independent.total_equiv` -/
460  def linear_independent.repr (hv : linear_independent R v) :
id                                                         
typ                                                        
461    span R (range v) →ₗ[R] ι →₀ R := hv.total_equiv.symm
id                             
typ                            
462  
463  lemma linear_independent.total_repr (x) : finsupp.total ι M R v (hv.repr x) = x :=
id                                                              
typ                                                             
464  subtype.coe_ext.1 (linear_equiv.apply_symm_apply hv.total_equiv x)
465  
466  lemma linear_independent.total_comp_repr : (finsupp.total ι M R v).comp hv.repr = submodule.subtype _ :=
id                                                                
typ                                                               
467  linear_map.ext $ hv.total_repr
468  
469  lemma linear_independent.repr_ker : hv.repr.ker = ⊥ :=
470  by rw [linear_independent.repr, linear_equiv.ker]
471  
472  lemma linear_independent.repr_range : hv.repr.range = ⊤ :=
473  by rw [linear_independent.repr, linear_equiv.range]
474  
475  lemma linear_independent.repr_eq
476    {l : ι →₀ R} {x} (eq : finsupp.total ι M R v l = ↑x) :
id                                           
typ                                          
477    hv.repr x = l :=
478  begin
479    have : ↑((linear_independent.total_equiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l)
480        = finsupp.total ι M R v l := rfl,
id                            
typ                           
481    have : (linear_independent.total_equiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x,
id                                                                            
typ                                                                           
482    { rw eq at this,
483      exact subtype.coe_ext.2 this },
st                                    └┘
484    rw ←linear_equiv.symm_apply_apply hv.total_equiv l,
485    rw ←this,
486    refl,
487  end
st   └─┘
488  
489  lemma linear_independent.repr_eq_single (i) (x) (hx : ↑x = v i) :
id                                                               
typ                                                              
490    hv.repr x = finsupp.single i 1 :=
id                                
typ                               
491  begin
492    apply hv.repr_eq,
493    simp [finsupp.total_single, hx]
494  end
st   └─┘
495  
496  lemma linear_independent_iff_not_smul_mem_span :
497    linear_independent R v ↔ (∀ (i : ι) (a : R), a • (v i) ∈ span R (v '' (univ \ {i})) → a = 0) :=
id                                                                                
src                           
typ                                                                               
498  ⟨ λ hv i a ha, begin
id           
typ          
499    rw [finsupp.span_eq_map_total, mem_map] at ha,
500    rcases ha with ⟨l, hl, e⟩,
501    rw sub_eq_zero.1 (linear_independent_iff.1 hv (l - finsupp.single i a) (by simp [e])) at hl,
id                                                                        
typ                                                                       
502    by_contra hn,
503    exact (not_mem_of_mem_diff (hl $ by simp [hn])) (mem_singleton _),
504  end, λ H, linear_independent_iff.2 $ λ l hl, begin
st   └─┘
505    ext i, simp,
506    by_contra hn,
507    refine hn (H i _ _),
id                  
typ                 
508    refine (finsupp.mem_span_iff_total _).2 ⟨finsupp.single i (l i) - l, _, _⟩,
id                                                                  
typ                                                                 
509    { rw finsupp.mem_supported',
510      intros j hj,
511      have hij : j = i :=
id                     
typ                    
512        classical.not_not.1
513            (λ hij : j ≠ i, hj ((mem_diff _).2 ⟨mem_univ _, λ h, hij (eq_of_mem_singleton h)⟩)),
id                         
typ                        
514      simp [hij] },
id             └─┘
typ            └─┘
st                  └┘
515    { simp [hl] }
st                 └─
516  end⟩
st   ──┘
517  
518  end repr
519  
520  lemma surjective_of_linear_independent_of_span
521    (hv : linear_independent R v) (f : ι' ↪ ι)
id                                      └┘   
typ                                     └┘   
522    (hss : range v ⊆ span R (range (v ∘ f))) (zero_ne_one : 0 ≠ (1 : R)):
id                                                                  
typ                                                                 
523    surjective f :=
id                
typ               
524  begin
525    intros i,
526    let repr : (span R (range (v ∘ f)) : Type*) → ι' →₀ R := (hv.comp f f.inj).repr,
id                                                 └┘    
typ                                                └┘    
527    let l := (repr ⟨v i, hss (mem_range_self i)⟩).map_domain f,
id                                                            
typ                                                           
528    have h_total_l : finsupp.total ι M R v l = v i,
id                                              
typ                                             
529    { dsimp only [l],
530      rw finsupp.total_map_domain,
531      rw (hv.comp f f.inj).total_repr,
532      { refl },
st              └┘
533      { exact f.inj } },
st                     └──┘
534    have h_total_eq : (finsupp.total ι M R v) l = (finsupp.total ι M R v) (finsupp.single i 1),
id                                                                                       
typ                                                                                      
535      by rw [h_total_l, finsupp.total_single, one_smul],
st                                                       
536    have l_eq : l = _ := linear_map.ker_eq_bot.1 hv h_total_eq,
537    dsimp only [l] at l_eq,
538    rw ←finsupp.emb_domain_eq_map_domain at l_eq,
539    rcases finsupp.single_of_emb_domain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with ⟨i', hi'⟩,
id                                                                      
typ                                                                     
540    use i',
id         └┘
typ        └┘
541    exact hi'.2
542  end
st   └─┘
543  
544  lemma eq_of_linear_independent_of_span_subtype {s t : set M} (zero_ne_one : (0 : R) ≠ 1)
id                                                                                   
typ                                                                                  
545    (hs : linear_independent R (λ x, x : s → M)) (h : t ⊆ s) (hst : s ⊆ span R t) : s = t :=
id                                                                                 
typ                                                                                
546  begin
547    let f : t ↪ s := ⟨λ x, ⟨x.1, h x.2⟩, λ a b hab, subtype.val_injective (subtype.mk.inj hab)⟩,
id               
src              
typ              
548    have h_surj : surjective f,
549    { apply surjective_of_linear_independent_of_span hs f _ zero_ne_one,
550      convert hst; simp [f, comp], },
st                                    └┘
551    show s = t,
id             
typ            
552    { apply subset.antisymm _ h,
553      intros x hx,
554      rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩,
id                      
typ                     
555      convert y.mem,
556      rw ← subtype.mk.inj hy,
557      refl }
st            └─
558  end
st   ──┘
559  
560  open linear_map
561  
562  lemma linear_independent.image (hv : linear_independent R v) {f : M →ₗ M'}
id                                                                       └┘
typ                                                                      └┘
563    (hf_inj : disjoint (span R (range v)) f.ker) : linear_independent R (f ∘ v) :=
id                                                                           
typ                                                                          
564  begin
565    rw [disjoint, ← set.image_univ, finsupp.span_eq_map_total, map_inf_eq_map_inf_comap,
566      map_le_iff_le_comap, comap_bot, finsupp.supported_univ, top_inf_eq] at hf_inj,
567    unfold linear_independent at hv,
568    rw hv at hf_inj,
569    haveI : inhabited M := ⟨0⟩,
id             └───────┘ 
src            └───────┘
typ            └───────┘ 
570    rw [linear_independent, finsupp.total_comp],
571    rw [@finsupp.lmap_domain_total _ _ R _ _ _ _ _ _ _ _ _ _ f, ker_comp, eq_bot_iff],
id                                        
typ                                       
572    apply hf_inj,
573    exact λ _, rfl,
id             
typ            
574  end
st   └─┘
575  
576  lemma linear_independent.image_subtype {s : set M} {f : M →ₗ M'} (hs : linear_independent R (λ x, x : s → M))
id                                               └┘             └┘                                          
src                                              └┘
typ                                              └┘             └┘                                          
577    (hf_inj : disjoint (span R s) f.ker) : linear_independent R (λ x, x : f '' s → M') :=
id                                                                                └┘
typ                                                                               └┘
578  begin
579    rw [disjoint, ← set.image_id s, finsupp.span_eq_map_total, map_inf_eq_map_inf_comap,
580      map_le_iff_le_comap, comap_bot] at hf_inj,
581    haveI : inhabited M := ⟨0⟩,
id             └───────┘ 
src            └───────┘
typ            └───────┘ 
582    rw [linear_independent_subtype_disjoint, disjoint, ← finsupp.lmap_domain_supported _ _ f, map_inf_eq_map_inf_comap,
583        map_le_iff_le_comap, ← ker_comp],
584    rw [@finsupp.lmap_domain_total _ _ R _ _ _, ker_comp],
id                                        
typ                                       
585    { exact le_trans (le_inf inf_le_left hf_inj) (le_trans (linear_independent_subtype_disjoint.1 hs) bot_le) },
st                                                                                                               └┘
586    { simp }
st            └─
587  end
st   ──┘
588  
589  lemma linear_independent_inl_union_inr {s : set M} {t : set M'}
id                                               └┘         └┘  └┘
src                                              └┘          └┘
typ                                              └┘         └┘  └┘
590    (hs : linear_independent R (λ x, x : s → M))
id                                             
typ                                            
591    (ht : linear_independent R (λ x, x : t → M')) :
id                                             └┘
typ                                            └┘
592    linear_independent R (λ x, x : inl R M M' '' s ∪ inr R M M' '' t → M × M') :=
id                                         └┘             └┘          
typ                                        └┘             └┘          
593  begin
594    apply linear_independent_union,
595    exact (hs.image_subtype $ by simp),
596    exact (ht.image_subtype $ by simp),
597    rw [span_image, span_image];
598      simp [disjoint_iff, prod_inf_prod]
599  end
st   └─┘
600  
601  lemma linear_independent_inl_union_inr' {v : ι → M} {v' : ι' → M'}
id                                                           └┘   └┘
typ                                                          └┘   └┘
602    (hv : linear_independent R v) (hv' : linear_independent R v') :
id                                                            └┘
typ                                                           └┘
603    linear_independent R (sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) :=
id                                          └┘            └┘   └┘
typ                                         └┘            └┘   └┘
604  begin
605    by_cases zero_eq_one : (0 : R) = 1,
606    { apply linear_independent_of_zero_eq_one zero_eq_one },
st                                                           └┘
607    have inj_v : injective v := (linear_independent.injective zero_eq_one hv),
id                            
typ                           
608    have inj_v' : injective v' := (linear_independent.injective zero_eq_one hv'),
id                             └┘
typ                            └┘
609    apply linear_independent.of_subtype_range,
610    { apply sum.elim_injective,
611      { exact injective_comp prod.injective_inl inj_v },
id                                                 └───┘
typ                                                └───┘
st                                                       └┘
612      { exact injective_comp prod.injective_inr inj_v' },
id                                                 └────┘
typ                                                └────┘
st                                                        └┘
613      { intros, simp [ne_zero_of_linear_independent zero_eq_one hv] } },
st                                                                     └──┘
614    { rw sum.elim_range,
615      apply linear_independent_union,
616      { apply linear_independent.to_subtype_range,
617        apply linear_independent.image hv,
618        simp [ker_inl] },
st                        └┘
619      { apply linear_independent.to_subtype_range,
620        apply linear_independent.image hv',
621        simp [ker_inr] },
st                        └┘
622      { apply disjoint_mono _ _ disjoint_inl_inr,
623        { rw [set.range_comp, span_image],
624          apply linear_map.map_le_range },
st                                         └┘
625        { rw [set.range_comp, span_image],
626          apply linear_map.map_le_range } } }
st                                         └─────
627  end
st   ──┘
628  
629  /-- Dedekind's linear independence of characters -/
630  -- See, for example, Keith Conrad's note <https://kconrad.math.uconn.edu/blurbs/galoistheory/linearchar.pdf>
631  theorem linear_independent_monoid_hom (G : Type*) [monoid G] (L : Type*) [integral_domain L] :
id                                                        └──┘                └──┘  └──┘  └─┘ 
src                                                       └──┘                 └──┘  └──┘  └─┘
typ                                                       └──┘                └──┘  └──┘  └─┘ 
632    @linear_independent _ L (G → L) (λ f, f : (G →* L) → (G → L)) _ _ _ :=
id                                                           
typ                                                          
633  by letI := classical.dec_eq (G →* L);
id                                    
typ                                   
634     letI : mul_action L L := distrib_mul_action.to_mul_action L L;
id                                                                 
typ                                                                
635  -- We prove linear independence by showing that only the trivial linear combination vanishes.
636  exact linear_independent_iff'.2
637  -- To do this, we use `finset` induction,
638  (λ s, finset.induction_on s (λ g hg i, false.elim) $ λ a s has ih g hg,
639  -- Here
640  -- * `a` is a new character we will insert into the `finset` of characters `s`,
641  -- * `ih` is the fact that only the trivial linear combination of characters in `s` is zero
642  -- * `hg` is the fact that `g` are the coefficients of a linear combination summing to zero
643  -- and it remains to prove that `g` vanishes on `insert a s`.
644  
645  -- We now make the key calculation:
646  -- For any character `i` in the original `finset`, we have `g i • i = g i • a` as functions on the monoid `G`.
647  have h1 : ∀ i ∈ s, (g i • i : G → L) = g i • a, from λ i his, funext $ λ x : G,
648    -- We prove these expressions are equal by showing
649    -- the differences of their values on each monoid element `x` is zero
650    eq_of_sub_eq_zero $ ih (λ j, g j * j x - g j * a x)
651      (funext $ λ y : G, calc
652      -- After that, it's just a chase scene.
653            s.sum (λ i, ((g i * i x - g i * a x) • i : G → L)) y
654          = s.sum (λ i, (g i * i x - g i * a x) * i y) : pi.finset_sum_apply _ _ _
655      ... = s.sum (λ i, g i * i x * i y - g i * a x * i y) : finset.sum_congr rfl
656        (λ _ _, sub_mul _ _ _)
657      ... = s.sum (λ i, g i * i x * i y) - s.sum (λ i, g i * a x * i y) : finset.sum_sub_distrib
658      ... = (g a * a x * a y + s.sum (λ i, g i * i x * i y))
659            - (g a * a x * a y + s.sum (λ i, g i * a x * i y)) : by rw add_sub_add_left_eq_sub
660      ... = (insert a s).sum (λ i, g i * i x * i y) - (insert a s).sum (λ i, g i * a x * i y) :
661        by rw [finset.sum_insert has, finset.sum_insert has]
st                                                            
662      ... = (insert a s).sum (λ i, g i * i (x * y)) - (insert a s).sum (λ i, a x * (g i * i y)) :
663        congr (congr_arg has_sub.sub (finset.sum_congr rfl $ λ i _, by rw [i.map_mul, mul_assoc]))
st                                                                                                
664          (finset.sum_congr rfl $ λ _ _, by rw [mul_assoc, mul_left_comm])
st                                                                         
665      ... = (insert a s).sum (λ i, (g i • i : G → L)) (x * y)
666            - a x * (insert a s).sum (λ i, (g i • i : G → L)) y :
667        by rw [pi.finset_sum_apply, pi.finset_sum_apply, finset.mul_sum]; refl
668      ... = 0 - a x * 0 : by rw hg; refl
669      ... = 0 : by rw [mul_zero, sub_zero])
st                                          
670      i
671      his,
672  -- On the other hand, since `a` is not already in `s`, for any character `i ∈ s`
673  -- there is some element of the monoid on which it differs from `a`.
674  have h2 : ∀ i : G →* L, i ∈ s → ∃ y, i y ≠ a y, from λ i his,
id                                     
typ                                    
675    classical.by_contradiction $ λ h,
676    have hia : i = a, from monoid_hom.ext $ λ y, classical.by_contradiction $ λ hy, h ⟨y, hy⟩,
id                                               
typ                                              
677    has $ hia ▸ his,
678  -- From these two facts we deduce that `g` actually vanishes on `s`,
679  have h3 : ∀ i ∈ s, g i = 0, from λ i his, let ⟨y, hy⟩ := h2 i his in
id                                                  
typ                                                 
680    have h : g i • i y = g i • a y, from congr_fun (h1 i his) y,
681    or.resolve_right (mul_eq_zero.1 $ by rw [mul_sub, sub_eq_zero]; exact h) (sub_ne_zero_of_ne hy),
682  -- And so, using the fact that the linear combination over `s` and over `insert a s` both vanish,
683  -- we deduce that `g a = 0`.
684  have h4 : g a = 0, from calc
685    g a = g a * 1 : (mul_one _).symm
686    ... = (g a • a : G → L) 1 : by rw ← a.map_one; refl
id                                                    └──┘
src                                                   └──┘
typ                                                   └──┘
doc                                                   └──┘
687    ... = (insert a s).sum (λ i, (g i • i : G → L)) 1 : begin
688        rw finset.sum_eq_single a,
689        { intros i his hia, rw finset.mem_insert at his, rw [h3 i (his.resolve_left hia), zero_smul] },
st                                                                                                     └┘
690        { intros haas, exfalso, apply haas, exact finset.mem_insert_self a s }
st                                                                              └┘
691      end
st       └─┘
692    ... = 0 : by rw hg; refl,
693  -- Now we're done; the last two facts together imply that `g` vanishes on every element of `insert a s`.
694  (finset.forall_mem_insert _ _ _).2 ⟨h4, h3⟩)
695  
696  lemma le_of_span_le_span {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
id                                                              
typ                                                             
697    (hl : linear_independent R (subtype.val : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u)
id                                                                            
typ                                                                           
698    (hst : span R s ≤ span R t) : s ⊆ t :=
id                                  
typ                                 
699  begin
700    have := eq_of_linear_independent_of_span_subtype zero_ne_one
701      (hl.mono (set.union_subset hsu htu))
702      (set.subset_union_right _ _)
703      (set.union_subset (set.subset.trans subset_span hst) subset_span),
704    rw ← this, apply set.subset_union_left
705  end
st   └─┘
706  
707  lemma span_le_span_iff {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
id                                                            
typ                                                           
708    (hl : linear_independent R (subtype.val : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u) :
id                                                                             
typ                                                                            
709    span R s ≤ span R t ↔ s ⊆ t :=
id                          
typ                         
710  ⟨le_of_span_le_span zero_ne_one hl hsu htu, span_mono⟩
711  
712  variables (R) (v)
713  /-- A family of vectors is a basis if it is linearly independent and all vectors are in the span. -/
714  def is_basis := linear_independent R v ∧ span R (range v) = ⊤
id                                                      
src                                         
typ                                                     
715  variables {R} {v}
716  
717  section is_basis
718  variables {s t : set M} (hv : is_basis R v)
719  
720  lemma is_basis.mem_span (hv : is_basis R v) : ∀ x, x ∈ span R (range v) := eq_top_iff'.1 hv.2
id                                                                   
typ                                                                  
721  
722  lemma is_basis.comp (hv : is_basis R v) (f : ι' → ι) (hf : bijective f) :
id                                              └┘                     
typ                                             └┘                     
723    is_basis R (v ∘ f) :=
id                   
typ                  
724  begin
725    split,
726    { apply hv.1.comp f hf.1 },
st                              └┘
727    { rw[set.range_comp, range_iff_surjective.2 hf.2, image_univ, hv.2] }
id                                                 └┘
typ                                                └┘
st                                                                        └─
728  end
st   ──┘
729  
730  lemma is_basis.injective (hv : is_basis R v) (zero_ne_one : (0 : R) ≠ 1) : injective v :=
id                                                                                     
typ                                                                                    
731    λ x y h, linear_independent.injective zero_ne_one hv.1 h
id        
typ       
732  
733  /- Given a basis, any vector can be written as a linear combination of the basis vectors. They are
734     given by this linear map. This is one direction of `module_equiv_finsupp` -/
735  def is_basis.repr : M →ₗ (ι →₀ R) :=
id                                
typ                               
736  (hv.1.repr).comp (linear_map.id.cod_restrict _ hv.mem_span)
737  
738  lemma is_basis.total_repr (x) : finsupp.total ι M R v (hv.repr x) = x :=
id                                                                  
typ                                                                 
739  hv.1.total_repr ⟨x, _⟩
id                    
typ                   
740  
741  lemma is_basis.total_comp_repr : (finsupp.total ι M R v).comp hv.repr = linear_map.id :=
id                                                      
typ                                                     
742  linear_map.ext hv.total_repr
743  
744  lemma is_basis.repr_ker : hv.repr.ker = ⊥ :=
745  linear_map.ker_eq_bot.2 $ injective_of_left_inverse hv.total_repr
746  
747  lemma is_basis.repr_range : hv.repr.range = finsupp.supported R R univ :=
id                                                                  
typ                                                                 
748  by rw [is_basis.repr, linear_map.range, submodule.map_comp,
749    linear_map.map_cod_restrict, submodule.map_id, comap_top, map_top, hv.1.repr_range,
750    finsupp.supported_univ]
st                           
751  
752  lemma is_basis.repr_total (x : ι →₀ R) (hx : x ∈ finsupp.supported R R (univ : set ι)) :
id                                                                              └┘  
src                                                                                 └┘
typ                                                                             └┘  
753    hv.repr (finsupp.total ι M R v x) = x :=
id                               
typ                              
754  begin
755    rw [← hv.repr_range, linear_map.mem_range] at hx,
756    cases hx with w hw,
757    rw [← hw, hv.total_repr],
st                            
758  end
st   └─┘
759  
760  lemma is_basis.repr_eq_single {i} : hv.repr (v i) = finsupp.single i 1 :=
id                                                                    
typ                                                                   
761  by apply hv.1.repr_eq_single; simp
762  
763  /-- Construct a linear map given the value at the basis. -/
764  def is_basis.constr (f : ι → M') : M →ₗ[R] M' :=
id                               └┘          └┘
typ                              └┘          └┘
765  (finsupp.total M' M' R id).comp $ (finsupp.lmap_domain R R f).comp hv.repr
id                  └┘ └┘                                    
typ                 └┘ └┘                                    
766  
767  theorem is_basis.constr_apply (f : ι → M') (x : M) :
id                                         └┘       
typ                                        └┘       
768    (hv.constr f : M → M') x = (hv.repr x).sum (λb a, a • f b) :=
id                      └┘                              
typ                     └┘                              
769  by dsimp [is_basis.constr];
770     rw [finsupp.total_apply, finsupp.sum_map_domain_index]; simp [add_smul]
771  
772  lemma is_basis.ext {f g : M →ₗ[R] M'} (hv : is_basis R v) (h : ∀i, f (v i) = g (v i)) : f = g :=
id                                   └┘                                        
typ                                  └┘                                        
773  begin
774    apply linear_map.ext (λ x, linear_eq_on (range v) _ (hv.mem_span x)),
775    exact (λ y hy, exists.elim (set.mem_range.1 hy) (λ i hi, by rw ←hi; exact h i))
id                                                        └┘         └┘          
typ                                                       └┘         └┘          
776  end
st   └─┘
777  
778  lemma constr_basis {f : ι → M'} {i : ι} (hv : is_basis R v) :
id                              └┘                         
typ                             └┘                         
779    (hv.constr f : M → M') (v i) = f i :=
id                      └┘         
typ                     └┘         
780  by simp [is_basis.constr_apply, hv.repr_eq_single, finsupp.sum_single_index]
781  
782  lemma constr_eq {g : ι → M'} {f : M →ₗ[R] M'} (hv : is_basis R v)
id                           └┘             └┘                  
typ                          └┘             └┘                  
783    (h : ∀i, g i = f (v i)) : hv.constr g = f :=
id                                     
typ                                    
784  hv.ext $ λ i, (constr_basis hv).trans (h i)
id                                           
typ                                          
785  
786  lemma constr_self (f : M →ₗ[R] M') : hv.constr (λ i, f (v i)) = f :=
id                                └┘                       
typ                               └┘                       
787  constr_eq hv $ λ x, rfl
id                    
typ                   
788  
789  lemma constr_zero (hv : is_basis R v) : hv.constr (λi, (0 : M')) = 0 :=
id                                                            └┘
typ                                                           └┘
790  constr_eq hv $ λ x, rfl
id                    
typ                   
791  
792  lemma constr_add {g f : ι → M'} (hv : is_basis R v) :
id                              └┘                  
typ                             └┘                  
793    hv.constr (λi, f i + g i) = hv.constr f + hv.constr g :=
id                                                   
typ                                                  
794  constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
id                                                           └┘
src                                                          └┘
typ                                                          └┘
795  
796  lemma constr_neg {f : ι → M'} (hv : is_basis R v) : hv.constr (λi, - f i) = - hv.constr f :=
id                            └┘                                                       
typ                           └┘                                                       
797  constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
id                                                           └┘
src                                                          └┘
typ                                                          └┘
798  
799  lemma constr_sub {g f : ι → M'} (hs : is_basis R v) :
id                              └┘                  
typ                             └┘                  
800    hv.constr (λi, f i - g i) = hs.constr f - hs.constr g :=
id                                                   
typ                                                  
801  by simp [constr_add, constr_neg]
802  
803  -- this only works on functions if `R` is a commutative ring
804  lemma constr_smul {ι R M M'} [comm_ring R]
id                                 └──┘  └─┘ 
src                                └──┘  └─┘
typ                                └──┘  └─┘ 
805    [add_comm_group M] [add_comm_group M'] [module R M] [module R M']
id       └┘ └┘ └┘ └┘      └──┘  └──┘   └┘                      └┘
src      └┘ └┘ └┘ └┘       └──┘  └──┘  
typ      └┘ └┘ └┘ └┘      └──┘  └──┘   └┘                      └┘
806    {v : ι → R} {f : ι → M'} {a : R} (hv : is_basis R v) {b : M} :
id                       └┘                                
typ                      └┘                                
807    hv.constr (λb, a • f b) = a • hv.constr f :=
id                                        
typ                                       
808  constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
id                                                           └┘
src                                                          └┘
typ                                                          └┘
809  
810  lemma constr_range [inhabited ι] (hv : is_basis R v) {f : ι  → M'} :
id                       └──┘  └─┘                              └┘
src                      └──┘  └─┘
typ                      └──┘  └─┘                              └┘
811    (hv.constr f).range = span R (range f) :=
id                                       
typ                                      
812  by rw [is_basis.constr, linear_map.range_comp, linear_map.range_comp, is_basis.repr_range,
813      finsupp.lmap_domain_supported, ←set.image_univ, ←finsupp.span_eq_map_total, image_id]
st                                                                                           
814  
815  /-- Canonical equivalence between a module and the linear combinations of basis vectors. -/
816  def module_equiv_finsupp (hv : is_basis R v) : M ≃ₗ[R] ι →₀ R :=
id                                                          
typ                                                         
817  (hv.1.total_equiv.trans (linear_equiv.of_top _ hv.2)).symm
818  
819  /-- Isomorphism between the two modules, given two modules M and M' with respective bases v and v'
820     and a bijection between the two bases. -/
821  def equiv_of_is_basis {v : ι → M} {v' : ι' → M'} {f : M → M'} {g : M' → M}
id                                         └┘              └┘       └┘
typ                                        └┘              └┘       └┘
822    (hv : is_basis R v) (hv' : is_basis R v') (hf : ∀i, f (v i) ∈ range v') (hg : ∀i, g (v' i) ∈ range v)
id                                        └┘                         └┘              └┘           
typ                                       └┘                         └┘              └┘           
823    (hgf : ∀i, g (f (v i)) = v i) (hfg : ∀i, f (g (v' i)) = v' i) :
id                                           └┘      └┘ 
typ                                          └┘      └┘ 
824    M ≃ₗ M' :=
id         └┘
typ        └┘
825  { inv_fun := hv'.constr (g ∘ v'),
id                                
typ                               
826    left_inv :=
827      have (hv'.constr (g ∘ v')).comp (hv.constr (f ∘ v)) = linear_map.id,
id                                                 
typ                                                
828      from hv.ext $ λ i, exists.elim (hf i) (λ i' hi', by simp [constr_basis, hi'.symm]; rw [hi', hgf]),
id                                              └┘
typ                                             └┘
st                                                                                                      
829      λ x, congr_arg (λ h:M →ₗ[R] M, h x) this,
id                                    
typ                                   
830    right_inv :=
831      have (hv.constr (f ∘ v)).comp (hv'.constr (g ∘ v')) = linear_map.id,
id                                                   └┘
typ                                                  └┘
832      from hv'.ext $ λ i', exists.elim (hg i') (λ i hi, by simp [constr_basis, hi.symm]; rw [hi, hfg]),
id                        └┘                  └┘     
typ                       └┘                  └┘     
st                                                                                                     
833      λ y, congr_arg (λ h:M' →ₗ[R] M', h y) this,
id                          └┘      └┘    
typ                         └┘      └┘    
834    ..hv.constr (f ∘ v) }
id                     
typ                    
835  
836  lemma is_basis_inl_union_inr {v : ι → M} {v' : ι' → M'}
id                                                └┘   └┘
typ                                               └┘   └┘
837    (hv : is_basis R v) (hv' : is_basis R v') : is_basis R (sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) :=
id                                        └┘                               └┘            └┘   └┘
typ                                       └┘                               └┘            └┘   └┘
838  begin
839    split,
840    apply linear_independent_inl_union_inr' hv.1 hv'.1,
841    rw [sum.elim_range, span_union,
842        set.range_comp, span_image (inl R M M'), hv.2,  map_top,
id                                           └┘
typ                                          └┘
843        set.range_comp, span_image (inr R M M'), hv'.2, map_top],
id                                           └┘
typ                                          └┘
844    exact linear_map.sup_range_inl_inr
845  end
st   └─┘
846  
847  end is_basis
848  
849  lemma is_basis_singleton_one (R : Type*) [unique ι] [ring R] :
id                                             └┘  └┘    └─┘  
src                                            └┘  └┘     └─┘
typ                                            └┘  └┘    └─┘  
850    is_basis R (λ (_ : ι), (1 : R)) :=
id                               
typ                              
851  begin
852    split,
853    { refine linear_independent_iff.2 (λ l, _),
854      rw [finsupp.unique_single l, finsupp.total_single, smul_eq_mul, mul_one],
855      intro hi,
856      simp [hi] },
st                 └┘
857    { refine top_unique (λ _ _, _),
id                            
typ                           
858      simp [submodule.mem_span_singleton] }
st                                           └─
859  end
st   ──┘
860  
861  protected lemma linear_equiv.is_basis (hs : is_basis R v)
id                                                         
typ                                                        
862    (f : M ≃ₗ[R] M') : is_basis R (f ∘ v) :=
id                └┘                   
typ               └┘                   
863  begin
864    split,
865    { apply @linear_independent.image _ _ _ _ _ _ _ _ _ _ hs.1 (f : M →ₗ[R] M'),
866      simp [linear_equiv.ker f] },
st                                 └┘
867    { rw set.range_comp,
868      have : span R ((f : M →ₗ[R] M') '' range v) = ⊤,
id                                 └┘           
typ                                └┘           
869      { rw [span_image (f : M →ₗ[R] M'), hs.2],
id                                   └┘
typ                                  └┘
870        simp },
st              └┘
871      exact this }
st                  └─
872  end
st   ──┘
873  
874  lemma is_basis_span (hs : linear_independent R v) :
id                                                 
typ                                                
875    @is_basis ι R (span R (range v)) (λ i : ι, ⟨v i, subset_span (mem_range_self _)⟩) _ _ _ :=
id                                             
typ                                            
876  begin
877  split,
878  { apply linear_independent_span hs },
st                                      └┘
879  { rw eq_top_iff',
880    intro x,
881    have h₁ : subtype.val '' set.range (λ i, subtype.mk (v i) _) = range v,
id                                                                         
typ                                                                        
882      by rw ←set.range_comp,
883    have h₂ : map (submodule.subtype _) (span R (set.range (λ i, subtype.mk (v i) _)))
id                                                               
typ                                                              
884                = span R (range v),
id                                
typ                               
885      by rw [←span_image, submodule.subtype_eq_val, h₁],
st                                                       
886    have h₃ : (x : M) ∈ map (submodule.subtype _) (span R (set.range (λ i, subtype.mk (v i) _))),
id                                                                                     
typ                                                                                    
887      by rw h₂; apply subtype.mem x,
888    rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩,
889    have h_x_eq_y : x = y,
890      by rw [subtype.coe_ext, ← hy₂]; simp,
891    rw h_x_eq_y,
892    exact hy₁ }
st               └─
893  end
st   ──┘
894  
895  lemma is_basis_empty (h_empty : ¬ nonempty ι) (h : ∀x:M, x = 0) : is_basis R (λ x : ι, (0 : M)) :=
id                                     └┘  └┘                                       
src                                    └┘  └┘
typ                                    └┘  └┘                                       
896  ⟨ linear_independent_empty_type h_empty,
id                                   └┘  └┘
typ                                  └┘  └┘
897    eq_top_iff'.2 $ assume x, (h x).symm ▸ submodule.zero_mem _ ⟩
id                                 
typ                                
898  
899  lemma is_basis_empty_bot (h_empty : ¬ nonempty ι) : is_basis R (λ _ : ι, (0 : (⊥ : submodule R M))) :=
id                                         └┘  └┘                                              
src                                        └┘  └┘
typ                                        └┘  └┘                                              
900  begin
901    apply is_basis_empty h_empty,
902    intro x,
903    apply subtype.ext.2,
904    exact (submodule.mem_bot R).1 (subtype.mem x),
id                              
typ                             
905  end
st   └─┘
906  
907  open fintype
908  variables [fintype ι] (h : is_basis R v)
id              └──┘  
src             └──┘  
typ             └──┘  
doc             └──┘  
909  
910  /-- A module over R with a finite basis is linearly equivalent to functions from its basis to R. -/
911  def equiv_fun_basis  : M ≃ₗ[R] (ι → R) :=
id                                    
typ                                   
912  linear_equiv.trans (module_equiv_finsupp h)
913    { to_fun := finsupp.to_fun,
914      add := λ x y, by ext; exact finsupp.add_apply,
915      smul := λ x y, by ext; exact finsupp.smul_apply,
id                 
typ                
916      ..finsupp.equiv_fun_on_fintype }
917  
918  theorem module.card_fintype [fintype R] [fintype M] :
id                                └──┘      └┘ └┘  
src                               └──┘       └┘ └┘ 
typ                               └──┘      └┘ └┘  
doc                               └──┘       └┘ └┘ 
919    card M = (card R) ^ (card ι) :=
id                             
typ                            
920  calc card M = card (ι → R)    : card_congr (equiv_fun_basis h).to_equiv
id                         
typ                        
921          ... = card R ^ card ι : card_fun
id                              
typ                             
922  
923  /-- Given a basis `v` indexed by `ι`, the canonical linear equivalence between `ι → R` and `M` maps
924  a function `x : ι → R` to the linear combination `∑_i x i • v i`. -/
925  @[simp] lemma equiv_fun_basis_symm_apply (x : ι → R) :
id                                                    
typ                                                   
doc    └──┘
926    (equiv_fun_basis h).symm x = finset.sum finset.univ (λi, x i • v i) :=
id                                                                 
typ                                                                
927  begin
928    change finsupp.sum
929        ((finsupp.equiv_fun_on_fintype.symm : (ι → R) ≃ (ι →₀ R)) x) (λ (i : ι) (a : R), a • v i)
930      = finset.sum finset.univ (λi, x i • v i),
931    dsimp [finsupp.equiv_fun_on_fintype, finsupp.sum],
932    rw finset.sum_filter,
933    refine finset.sum_congr rfl (λi hi, _),
id                                   
typ                                  
934    by_cases H : x i = 0,
id                   
typ                  
935    { simp [H] },
st                └┘
936    { simp [H], refl }
st                      └─
937  end
st   ──┘
938  
939  end module
940  
941  section vector_space
942  variables
943    {v : ι → V}
944    [discrete_field K] [add_comm_group V] [add_comm_group V']
id        └┘  └┘  └┘       └┘ └┘ └┘ └┘ └┘
src       └┘  └┘  └┘       └┘ └┘ └┘ └┘ └┘
typ       └┘  └┘  └┘       └┘ └┘ └┘ └┘ └┘
945    [vector_space K V] [vector_space K V']
946    {s t : set V} {x y z : V}
947  include K
948  open submodule
949  
950  /- TODO: some of the following proofs can generalized with a zero_ne_one predicate type class
951     (instead of a data containing type class) -/
952  
953  section
954  set_option class.instance_max_depth 36
doc             └──────────────────────┘
955  
956  lemma mem_span_insert_exchange : x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s) :=
id                                                                                        
typ                                                                                       
957  begin
958    simp [mem_span_insert],
959    rintro a z hz rfl h,
960    refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, _⟩,
id                        
typ                       
961    have a0 : a ≠ 0, {rintro rfl, simp * at *},
id               
typ              
st                                              └┘
962    simp [a0, smul_add, smul_smul]
963  end
st   └─┘
964  
965  end
966  
967  lemma linear_independent_iff_not_mem_span : linear_independent K v ↔ (∀i, v i ∉ span K (v '' (univ \ {i}))) :=
id                                                                                                  
src                                                                     
typ                                                                                                 
968  begin
969    apply linear_independent_iff_not_smul_mem_span.trans,
970    split,
971    { intros h i h_in_span,
972      apply one_ne_zero (h i 1 (by simp [h_in_span])) },
id                            
typ                           
st                                                       └┘
973    { intros h i a ha,
974      by_contradiction ha',
975      exact false.elim (h _ ((smul_mem_iff _ ha').1 ha)) }
st                                                          └─
976  end
st   ──┘
977  
978  lemma linear_independent_unique [unique ι] (h : v (default ι) ≠ 0): linear_independent K v :=
id                                    └──┘                                                
src                                   └──┘
typ                                   └──┘                                                
979  begin
980    rw linear_independent_iff,
981    intros l hl,
982    ext i,
983    rw [unique.eq_default i, finsupp.zero_apply],
id                           
typ                          
984    by_contra hc,
985    have := smul_smul (l (default ι))⁻¹ (l (default ι)) (v (default ι)),
id                                                                    
typ                                                                   
986    rw [finsupp.unique_single l, finsupp.total_single] at hl,
987    rw [hl, inv_mul_cancel hc, smul_zero, one_smul] at this,
988    exact h this.symm
989  end
st   └─┘
990  
991  lemma linear_independent_singleton {x : V} (hx : x ≠ 0) : linear_independent K (λ x, x : ({x} : set V) → V) :=
id                                                                                                       
src                                                                                                    
typ                                                                                                      
992  begin
993    apply @linear_independent_unique _ _ _ _ _ _ _ _ _,
994    apply set.unique_singleton,
995    apply hx,
996  end
st   └─┘
997  
998  lemma disjoint_span_singleton {p : submodule K V} {x : V} (x0 : x ≠ 0) :
id                                                                
typ                                                               
999    disjoint p (span K {x}) ↔ x ∉ p :=
id                            
src                            
typ                           
1000  ⟨λ H xp, x0 (disjoint_def.1 H _ xp (singleton_subset_iff.1 subset_span:_)),
1001  begin
1002    simp [disjoint_def, mem_span_singleton],
1003    rintro xp y yp a rfl,
1004    by_cases a0 : a = 0, {simp [a0]},
id                   
typ                  
st                                    └┘
1005    exact xp.elim ((smul_mem_iff p a0).1 yp),
1006  end⟩
st   └─┘
1007  
1008  lemma linear_independent.insert (hs : linear_independent K (λ b, b : s → V)) (hx : x ∉ span K s) :
id                                                                                             
typ                                                                                            
1009    linear_independent K (λ b, b : insert x s → V) :=
id                                              
typ                                             
1010  begin
1011    rw ← union_singleton,
1012    have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem _) hx,
id               
typ              
1013    apply linear_independent_union hs (linear_independent_singleton x0),
1014    rwa [disjoint_span_singleton x0]
1015  end
st   └─┘
1016  
1017  lemma exists_linear_independent (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ t) :
id                                                                                        
typ                                                                                       
1018    ∃b⊆t, s ⊆ b ∧ t ⊆ span K b ∧ linear_independent K (λ x, x : b → V) :=
id                                                              
typ                                                             
1019  begin
1020    rcases zorn.zorn_subset₀ {b | b ⊆ t ∧ linear_independent K (λ x, x : b → V)} _ _
id                                                                           
typ                                                                          
1021      ⟨hst, hs⟩ with ⟨b, ⟨bt, bi⟩, sb, h⟩,
1022    { refine ⟨b, bt, sb, λ x xt, _, bi⟩,
id                           
typ                          
1023      haveI := classical.dec (x ∈ span K b),
id                └───────────┘           
src               └───────────┘
typ               └───────────┘           
1024      by_contra hn,
1025      apply hn,
1026      rw ← h _ ⟨insert_subset.2 ⟨xt, bt⟩, bi.insert hn⟩ (subset_insert _ _),
1027      exact subset_span (mem_insert _ _) },
st                                          └┘
1028    { refine λ c hc cc c0, ⟨⋃₀ c, ⟨_, _⟩, λ x, _⟩,
id                       └┘                   
typ                      └┘                   
1029      { exact sUnion_subset (λ x xc, (hc xc).1) },
id                                
typ                               
st                                                 └┘
1030      { exact linear_independent_sUnion_of_directed cc.directed_on (λ x xc, (hc xc).2) },
id                                                                       
typ                                                                      
st                                                                                        └┘
1031      { exact subset_sUnion_of_mem } }
st                                    └───
1032  end
st   ──┘
1033  
1034  lemma exists_subset_is_basis (hs : linear_independent K (λ x, x : s → V)) :
id                                                                        
typ                                                                       
1035    ∃b, s ⊆ b ∧ is_basis K (λ i : b, i.val) :=
id                      
src              
typ                     
1036  let ⟨b, hb₀, hx, hb₂, hb₃⟩ := exists_linear_independent hs (@subset_univ _ _) in
id        
typ       
1037  ⟨ b, hx,
1038    @linear_independent.restrict_of_comp_subtype _ _ _ id _ _ _ _ hb₃,
1039    by simp; exact eq_top_iff.2 hb₂⟩
1040  
1041  variables (K V)
1042  lemma exists_is_basis : ∃b : set V, is_basis K (λ i : b, i.val) :=
id                                               
typ                                              
1043  let ⟨b, _, hb⟩ := exists_subset_is_basis linear_independent_empty in ⟨b, hb⟩
id        
typ       
1044  
1045  variables {K V}
1046  
1047  -- TODO(Mario): rewrite?
1048  lemma exists_of_linear_independent_of_finite_span {t : finset V}
id                                                            └┘   
src                                                           └┘
typ                                                           └┘   
doc                                                           └┘
1049    (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ (span K ↑t : submodule K V)) :
id                                                                                
typ                                                                               
1050    ∃t':finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card :=
id                   └┘             └┘   └┘        
src                               
typ                  └┘             └┘   └┘        
1051  have ∀t, ∀(s' : finset V), ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ (span K ↑(s' ∪ t) : submodule K V) →
id                             └┘                               └┘                 
typ                            └┘                               └┘                 
1052    ∃t':finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
id                   └┘                 └┘             
src                                         
typ                  └┘                 └┘             
1053  assume t, finset.induction_on t
id                                
typ                               
1054    (assume s' hs' _ hss',
id             └┘
typ            └┘
1055      have s = ↑s',
id                └┘
typ               └┘
1056        from eq_of_linear_independent_of_span_subtype (@zero_ne_one K _) hs hs' $
id                                                                     
typ                                                                    
1057            by simpa using hss',
1058      ⟨s', by simp [this]⟩)
id        └┘
typ       └┘
1059    (assume b₁ t hb₁t ih s' hs' hst hss',
id             └┘          └┘
typ            └┘          └┘
1060      have hb₁s : b₁ ∉ s,
id                   └┘   
typ                  └┘   
1061        from assume h,
1062        have b₁ ∈ s ∩ ↑(insert b₁ t), from ⟨h, finset.mem_insert_self _ _⟩,
id              └┘               └┘ 
typ             └┘               └┘ 
1063        by rwa [hst] at this,
1064      have hb₁s' : b₁ ∉ s', from assume h, hb₁s $ hs' h,
id                    └┘   └┘
typ                   └┘   └┘
1065      have hst : s ∩ ↑t = ∅,
id                      
typ                     
1066        from eq_empty_of_subset_empty $ subset.trans
1067          (by simp [inter_subset_inter, subset.refl]) (le_of_eq hst),
1068      classical.by_cases
1069        (assume : s ⊆ (span K ↑(s' ∪ t) : submodule K V),
id                               └┘                  
typ                              └┘                  
1070          let ⟨u, hust, hsu, eq⟩ := ih _ hs' hst this in
id                
typ               
1071          have hb₁u : b₁ ∉ u, from assume h, (hust h).elim hb₁s hb₁t,
id                       └┘
typ                      └┘
1072          ⟨insert b₁ u, by simp [insert_subset_insert hust],
id                   └┘
typ                  └┘
1073            subset.trans hsu (by simp), by simp [eq, hb₁t, hb₁s', hb₁u]⟩)
1074        (assume : ¬ s ⊆ (span K ↑(s' ∪ t) : submodule K V),
id                                 └┘                  
typ                                └┘                  
1075          let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this in
id                └┘
typ               └┘
1076          have hb₂t' : b₂ ∉ s' ∪ t, from assume h, hb₂t $ subset_span h,
id                             └┘   
typ                            └┘   
1077          have s ⊆ (span K ↑(insert b₂ s' ∪ t) : submodule K V), from
id                                      └┘                  
typ                                     └┘                  
1078            assume b₃ hb₃,
id                    └┘
typ                   └┘
1079            have ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : set V),
id                    └┘          └┘            └┘              └┘       └─┘ 
src                                                                        └─┘
typ                   └┘          └┘            └┘              └┘       └─┘ 
1080              by simp [insert_eq, -singleton_union, -union_singleton, union_subset_union, subset.refl, subset_union_right],
1081            have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : set V)),
id                        └┘                 └┘              └┘       └─┘ 
src                                                                     └─┘
typ                       └┘                 └┘              └┘       └─┘ 
1082              from span_mono this (hss' hb₃),
1083            have s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : submodule K V),
id                                    └┘   └┘                   
typ                                   └┘   └┘                   
1084              by simpa [insert_eq, -singleton_union, -union_singleton] using hss',
1085            have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)),
id                        └┘                      └┘   
typ                       └┘                      └┘   
1086              from mem_span_insert_exchange (this hb₂s) hb₂t,
1087            by rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃,
1088          let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset, hb₂s, hs']) hst this in
id                
typ               
1089          ⟨u, subset.trans hust $ union_subset_union (subset.refl _) (by simp [subset_insert]),
1090            hsu, by rw [finset.union_comm] at hb₂t'; simp [eq, hb₂t', hb₁t, hb₁s']⟩)),
1091  begin
1092    letI := classical.dec_pred (λx, x ∈ s),
id                                        
typ                                       
1093    have eq : t.filter (λx, x ∈ s) ∪ t.filter (λx, x ∉ s) = t,
id                                                          
typ                                                         
1094    { apply finset.ext.mpr,
1095      intro x,
1096      by_cases x ∈ s; simp *, finish },
id                   
typ                  
st                                      └┘
1097    apply exists.elim (this (t.filter (λx, x ∉ s)) (t.filter (λx, x ∈ s))
id                                                                     
typ                                                                    
1098      (by simp [set.subset_def]) (by simp [set.ext_iff] {contextual := tt}) (by rwa [eq])),
id                                                                        └┘
src                                                                       └┘
typ                                                                       └┘
1099    intros u h,
1100    exact ⟨u, subset.trans h.1 (by simp [subset_def, and_imp, or_imp_distrib] {contextual:=tt}),
id                                                                                           └┘
src                                                                                           └┘
typ                                                                                          └┘
1101      h.2.1, by simp only [h.2.2, eq]⟩
1102  end
st   └─┘
1103  
1104  lemma exists_finite_card_le_of_finite_of_linear_independent_of_span
1105    (ht : finite t) (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ span K t) :
id                                                                               
typ                                                                              
1106    ∃h : finite s, h.to_finset.card ≤ ht.to_finset.card :=
id                                     └┘
typ                                    └┘
1107  have s ⊆ (span K ↑(ht.to_finset) : submodule K V), by simp; assumption,
id                                                           └────────┘
src                                                              └────────┘
typ                                                          └────────┘
doc                                                              └────────┘
1108  let ⟨u, hust, hsu, eq⟩ := exists_of_linear_independent_of_finite_span hs this in
id        
typ       
1109  have finite s, from finite_subset u.finite_to_set hsu,
id               
typ              
1110  ⟨this, by rw [←eq]; exact (finset.card_le_of_subset $ finset.coe_subset.mp $ by simp [hsu])⟩
id    └──┘
typ   └──┘
1111  
1112  lemma exists_left_inverse_linear_map_of_injective {f : V →ₗ[K] V'}
id                                                                └┘
typ                                                               └┘
1113    (hf_inj : f.ker = ⊥) : ∃g:V' →ₗ V, g.comp f = linear_map.id :=
id                               └┘    
typ                              └┘    
1114  begin
1115    rcases exists_is_basis K V with ⟨B, hB⟩,
id                             
typ                            
1116    have hB₀ : _ := hB.1.to_subtype_range,
1117    have : linear_independent K (λ x, x : f '' B → V'),
id                                                  └┘
typ                                                 └┘
1118    { have h₁ := hB₀.image_subtype (show disjoint (span K (range (λ i : B, i.val))) (linear_map.ker f), by simp [hf_inj]),
id                                                         
typ                                                        
1119      have h₂ : range (λ (i : B), i.val) = B := subtype.range_val B,
id                                                                   
typ                                                                  
1120      rwa h₂ at h₁ },
st                    └┘
1121    rcases exists_subset_is_basis this with ⟨C, BC, hC⟩,
1122    haveI : inhabited V := ⟨0⟩,
id             └───────┘ 
src            └───────┘
typ            └───────┘ 
1123    use hC.constr (function.restrict (inv_fun f) C : C → V),
id                                                          
typ                                                         
1124    apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hB,
1125    intros b,
1126    rw image_subset_iff at BC,
1127    simp,
1128    have := BC (subtype.mem b),
1129    rw mem_preimage at this,
1130    have : f (b.val) = (subtype.mk (f ↑b) (begin rw ←mem_preimage, exact BC (subtype.mem b) end) : C).val,
id                                                                                                    
typ                                                                                                   
st                                                                                             └─┘
1131      by simp; unfold_coes,
1132    rw this,
1133    rw [constr_basis hC],
1134    exact left_inverse_inv_fun (linear_map.ker_eq_bot.1 hf_inj) _,
1135  end
st   └─┘
1136  
1137  lemma exists_right_inverse_linear_map_of_surjective {f : V →ₗ[K] V'}
id                                                                  └┘
typ                                                                 └┘
1138    (hf_surj : f.range = ⊤) : ∃g:V' →ₗ V, f.comp g = linear_map.id :=
id                                  └┘    
typ                                 └┘    
1139  begin
1140    rcases exists_is_basis K V' with ⟨C, hC⟩,
id                             └┘
typ                            └┘
1141    haveI : inhabited V := ⟨0⟩,
id             └───────┘ 
src            └───────┘
typ            └───────┘ 
1142    use hC.constr (function.restrict (inv_fun f) C : C → V),
id                                                          
typ                                                         
1143    apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hC,
1144    intros c,
1145    simp [constr_basis hC],
1146    exact right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) _
1147  end
st   └─┘
1148  
1149  set_option class.instance_max_depth 49
doc             └──────────────────────┘
1150  open submodule linear_map
1151  theorem quotient_prod_linear_equiv (p : submodule K V) :
id                                                      
typ                                                     
1152    nonempty ((p.quotient × p) ≃ₗ[K] V) :=
id     └┘  └┘                         
src    └┘  └┘                
typ    └┘  └┘                         
1153  begin
1154    haveI := classical.dec_eq (quotient p),
1155    rcases exists_right_inverse_linear_map_of_surjective p.range_mkq with ⟨f, hf⟩,
1156    have mkf : ∀ x, submodule.quotient.mk (f x) = x := linear_map.ext_iff.1 hf,
1157    have fp : ∀ x, x - f (p.mkq x) ∈ p :=
id                 
typ                
1158      λ x, (submodule.quotient.eq p).1 (mkf (p.mkq x)).symm,
id         
typ        
1159    refine ⟨linear_equiv.of_linear (f.copair p.subtype)
1160      (p.mkq.pair (cod_restrict p (linear_map.id - f.comp p.mkq) fp))
1161      (by ext; simp) _⟩,
1162    ext ⟨⟨x⟩, y, hy⟩; simp,
1163    { apply (submodule.quotient.eq p).2,
1164      simpa using sub_mem p hy (fp x) },
id                                    
typ                                   
st                                       └┘
1165    { refine subtype.coe_ext.2 _,
1166      simp [mkf, (submodule.quotient.mk_eq_zero p).2 hy] }
st                                                          └─
1167  end
st   ──┘
1168  
1169  open fintype
1170  
1171  theorem vector_space.card_fintype [fintype K] [fintype V] :
id                                      └┘  └─┘     └┘ └┘  
src                                     └┘  └─┘      └┘ └┘
typ                                     └┘  └─┘     └┘ └┘  
doc                                     └┘  └─┘      └┘ └┘
1172    ∃ n : ℕ, card V = (card K) ^ n :=
id                               
src          
typ                              
1173  begin
1174    apply exists.elim (exists_is_basis K V),
1175    intros b hb,
1176    haveI := classical.dec_pred (λ x, x ∈ b),
id                                          
typ                                         
1177    use card b,
id              
typ             
1178    exact module.card_fintype hb,
1179  end
st   └─┘
1180  
1181  end vector_space
1182  
1183  namespace pi
1184  open set linear_map
1185  
1186  section module
1187  variables {η : Type*} {ιs : η → Type*} {Ms : η → Type*}
id                                          
typ                                         
1188  variables [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)] [fintype η]
id                └┘                                                    └─────┘
src               └┘                                                       └─────┘
typ               └┘                                                    └─────┘
doc                                                                        └─────┘
1189  
1190  lemma linear_independent_std_basis
1191    (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) :
id             └┘                                           
typ            └┘                                           
1192    linear_independent R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (v ji.1 ji.2)) :=
id                                                     
typ                                                    
1193  begin
1194    have hs' : ∀j : η, linear_independent R (λ i : ιs j, std_basis R Ms j (v j i)),
id                                                                    └┘
typ                                                                   └┘
1195    { intro j,
1196      apply linear_independent.image (hs j),
id                                          
typ                                         
1197      simp [ker_std_basis] },
st                            └┘
1198    apply linear_independent_Union_finite hs',
1199    { assume j J _ hiJ,
1200      simp [(set.Union.equations._eqn_1 _).symm, submodule.span_image, submodule.span_Union],
1201      have h₀ : ∀ j, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
id                                           └┘
typ                                          └┘
1202          ≤ range (std_basis R Ms j),
id                               └┘
typ                              └┘
1203      { intro j,
1204        rw [span_le, linear_map.range_coe],
1205        apply range_comp_subset_range },
st                                       └┘
1206      have h₁ : span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
id                                       └┘
typ                                      └┘
1207          ≤ ⨆ i ∈ {j}, range (std_basis R Ms i),
id                                        └┘
typ                                       └┘
1208      { rw @supr_singleton _ _ _ (λ i, linear_map.range (std_basis R (λ (j : η), Ms j) i)),
id                                                                               └┘
typ                                                                              └┘
1209        apply h₀ },
st                  └┘
1210      have h₂ : (⨆ j ∈ J, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))) ≤
id                                                └┘
typ                                               └┘
1211                 ⨆ j ∈ J, range (std_basis R (λ (j : η), Ms j) j) :=
id                                                      └┘
typ                                                     └┘
1212        supr_le_supr (λ i, supr_le_supr (λ H, h₀ i)),
id                         
typ                        
1213      have h₃ : disjoint (λ (i : η), i ∈ {j}) J,
id                                             
typ                                            
1214      { convert set.disjoint_singleton_left.2 hiJ,
1215        rw ←@set_of_mem_eq _ {j},
id                               
typ                              
1216        refl },
st              └┘
1217      refine disjoint_mono h₁ h₂
1218        (disjoint_std_basis_std_basis _ _ _ _ h₃), }
st                                                    └─
1219  end
st   ──┘
1220  
1221  lemma is_basis_std_basis (s : Πj, ιs j → (Ms j)) (hs : ∀j, is_basis R (s j)) :
id                                    └┘                                 
typ                                   └┘                                 
1222    is_basis R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (s ji.1 ji.2)) :=
id                                           
typ                                          
1223  begin
1224    split,
1225    { apply linear_independent_std_basis _ (assume i, (hs i).1) },
st                                                                 └┘
1226    have h₁ : Union (λ j, set.range (std_basis R Ms j ∘ s j))
id                        
typ                       
1227      ⊆ range (λ (ji : Σ (j : η), ιs j), (std_basis R Ms (ji.fst)) (s (ji.fst) (ji.snd))),
id                                  └┘                 └┘
typ                                 └┘                 └┘
1228    { apply Union_subset, intro i,
1229      apply range_comp_subset_range (λ x : ιs i, (⟨i, x⟩ : Σ (j : η), ιs j))
id                                                    
typ                                                   
1230          (λ (ji : Σ (j : η), ιs j), std_basis R Ms (ji.fst) (s (ji.fst) (ji.snd))) },
id                                                └┘
typ                                               └┘
st                                                                                     └┘
1231    have h₂ : ∀ i, span R (range (std_basis R Ms i ∘ s i)) = range (std_basis R Ms i),
id                                                                               └┘
typ                                                                              └┘
1232    { intro i,
1233      rw [set.range_comp, submodule.span_image, (assume i, (hs i).2), submodule.map_top] },
id                                                         
typ                                                        
st                                                                                         └┘
1234    apply eq_top_mono,
1235    apply span_mono h₁,
1236    rw span_Union,
1237    simp only [h₂],
1238    apply supr_range_std_basis
1239  end
st   └─┘
1240  
1241  section
1242  variables (R η)
1243  
1244  lemma is_basis_fun₀ : is_basis R
id                                  
typ                                 
1245      (λ (ji : Σ (j : η), (λ _, unit) j),
id                               └──┘  
src                                └──┘
typ                              └──┘  
doc                                └──┘
1246         (std_basis R (λ (i : η), R) (ji.fst)) 1) :=
id                                 
typ                                
1247  begin
1248    haveI := classical.dec_eq,
1249    apply @is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ (λ _ _, (1 : R))
id                                          └──┘                               
src                                         └──┘
typ                                         └──┘                               
doc                                         └──┘
1250        (assume i, @is_basis_singleton_one _ _ _ _),
id                 
typ                
1251  end
st   └─┘
1252  
1253  lemma is_basis_fun : is_basis R (λ i, std_basis R (λi:η, R) i 1) :=
id                                                          
typ                                                         
1254  begin
1255    apply is_basis.comp (is_basis_fun₀ R η) (λ i, ⟨i, punit.star⟩),
1256    apply bijective_iff_has_inverse.2,
1257    use (λ x, x.1),
1258    simp [function.left_inverse, function.right_inverse],
1259    intros _ b,
1260    rw [unique.eq_default b, unique.eq_default punit.star]
id                                               └────────┘
src                                               └────────┘
typ                                              └────────┘
st                                                          
1261  end
st   └─┘
1262  
1263  end
1264  
1265  end module
1266  
1267  end pi